Stream: Coq users

Topic: ✔ Ltac1 matching on lambda


view this post on Zulip Lef Ioannidis (Oct 10 2023 at 00:27):

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.

view this post on Zulip Notification Bot (Oct 10 2023 at 00:38):

Lef Ioannidis has marked this topic as resolved.

view this post on Zulip Paolo Giarrusso (Oct 10 2023 at 02:23):

What was the solution?


Last updated: Jun 23 2024 at 03:02 UTC