In the docs about the
match tactic (not
match goal it says that the discriminant has to evaluate to a term, the only way that I were able to sue this tactic was in something like this
Lemma foo : True. set (x := 1). match x with | ?x => idtac x end.
I don't know what patterns I can try to match.
I see that this is possible
match type of HFoo with | some type => do something end.
Which would be useful when you have multiple goals where the same hypothesis (same name) appears but you want to apply it only if has some particular type shape, but I couldn't come up with other examples. The
match goal tactic I already use a lot and it's really useful but I can't see the use case of the
If you need to match on results of ltac computations, rather than terms that appear in the goal directly, you need match.
for instance, if you wanted to loop over hypotheses, reduce their type to
eval hnf in T (without modifying the original context), and dispatch on the result
(FWIW, if this comes up, it probably means your ltac automation is complex enough that it might be worth looking into Ltac2 — but the cost of transition is large since documentation is limited)
oh it's about ltac computations, now I get it, this is why
match x was not making sense, is more about
match some_tactic x
Now I remember a use case from another answer, like this
Ltac head f := match f with | ?g _ => head g | _ => f end.
Cool thanks Paolo!
This context switching betnween Ltac and Gallina makes me feel very confused sometimes
I don't know if you can write
match some_tactic x, I've only used
let y := some_tactic x in match y :-)
Last updated: Jan 29 2023 at 04:05 UTC