How can I match on a (constant) lambda in Ltac?
Here's a reproducible example, the "NOT FOUND" idtac is never printed and I am not sure why. The match falls through to the catch-all
Inductive applies{X}(f: X -> Prop) : X -> Prop :=
| Doapply : forall x,
f x -> applies f x.
Goal (applies (fun (b: unit) => True) tt -> True).
intro HH;
match type of HH with
| applies ?p ?x =>
match p with
| (fun _: unit => True) => idtac "NOT FOUND"
| ?c => idtac "Hit the catch all" ; idtac c
end
end.
Lef Ioannidis has marked this topic as resolved.
What was the solution?
Last updated: Oct 13 2024 at 01:02 UTC