Open dranov opened 6 months ago
I tried implementing this, but ran into an issue with term
taking over the case for ident
when defining the elab_rules
– I think there must be some way of properly defining priorities, but I couldn't figure it out.
I don't know how to resolve this issue with precedence. For now, if you want to revert a term t
, just put it inside parentheses:
elim: s ([]) Hnil=> [|x s2 IHs] s1 Hs1
Time permitting, let's extract the minimal example and post a question on Zulip
In the proof of
last_ind
inSeq.v
, one needs to generalize a term[]
. This is done byelim: s [] Hnil
, but this is currently not supported in Ssrlean.Here's the equivalent Lean proof: