Ssreflect Users Discussion List

[Georges Gonthier <>]

  Hello Arthur,

  there isn’t anything predefined along those lines. Your immediate options would be to hide the call to (erefl _) in a Notation (as in the [tnth t i] form),

or use the inord injection (lighter syntax, but you’ll need to rewrite with inordK then (leq_trans (ltn_ord _)) to eliminate it, so it’s a toss-up).

 

  cheers,

 

Georges

---

From: Arthur Azevedo de Amorim [mailto:]
Sent: 16 June 2009 16:21
To:
Subject: Automatic proofs of is_true

 

Hello everyone,

is there a way in plain ssr to cast between I_n and I_m when (n <= m) is convertible to true without mentioning explicitly its proof, e.g, when using a value of I_3 in a context that asks for an I_5 without calling widen_ord and passing it (refl_equal _)?

Thanks in advance.

--
Arthur Azevedo de Amorim