Can anybody give me a reason why this code would match
match goal with |[|- context[sum_rect _ _ _ (inl _)] ] => idtac end.
but this wouldn't match
match goal with |[|- context[sum_rect _ _ _ (inl ?var)] ] => idtac end.
i'm not sure i understand the difference between how holes and variables work in ltac.
Probably the occurrence of ?var is under binders like lambda?
Ok, that makes sense, maybe that is it.
I'll keep that in mind.
That's fixable, IIRC you must use ltac "second-order pattern matching"
https://github.com/tchajed/coq-tricks has one example involving it
Last updated: Sep 23 2023 at 13:01 UTC