Patrick Nicodemus (Jan 16 2022 at 22:52): Patrick Nicodemus (Jan 16 2022 at 22:52):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.
Paolo Giarrusso (Jan 17 2022 at 05:57):Probably the occurrence of ?var is under binders like lambda?
Patrick Nicodemus (Jan 17 2022 at 06:03):Ok, that makes sense, maybe that is it.
I'll keep that in mind.
Paolo Giarrusso (Jan 17 2022 at 06:39):That's fixable, IIRC you must use ltac "second-order pattern matching"
Paolo Giarrusso (Jan 17 2022 at 06:41):https://github.com/tchajed/coq-tricks has one example involving it
Last updated: Sep 23 2023 at 13:01 UTC