Stream: Coq users

Topic: Tactic to return the whole goal?


view this post on Zulip Daniel Hilst Selli (Aug 23 2022 at 20:26):

some times I write a tactic that walk over an expression and when I want to apply it to the whole goal I do something like this

match goal with
| |- ?goal => my_tactic goal
end.

Is there a better alternative to get the whole goal without this match?

view this post on Zulip Paolo Giarrusso (Aug 24 2022 at 02:17):

That seems good


Last updated: Feb 06 2023 at 11:03 UTC