Stream: Coq users

Topic: Holes vs bound variables


view this post on Zulip 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.

view this post on Zulip Paolo Giarrusso (Jan 17 2022 at 05:57):

Probably the occurrence of ?var is under binders like lambda?

view this post on Zulip Patrick Nicodemus (Jan 17 2022 at 06:03):

Ok, that makes sense, maybe that is it.
I'll keep that in mind.

view this post on Zulip Paolo Giarrusso (Jan 17 2022 at 06:39):

That's fixable, IIRC you must use ltac "second-order pattern matching"

view this post on Zulip Paolo Giarrusso (Jan 17 2022 at 06:41):

https://github.com/tchajed/coq-tricks has one example involving it


Last updated: Feb 01 2023 at 11:04 UTC