Stream: Coq users

Topic: Can't match on `constr_under_binder`?


view this post on Zulip Li-yao (Mar 21 2024 at 11:45):

Does ltac match/lazymatch not work for open terms (constr_under_binder)?

Ltac f M :=
  match M with
  | (fun x => ?M) => f M
  | _ => idtac M
  end.

Goal False. let M := f (fun x => x) in idtac M.

(* Error:
Must evaluate to a closed term
offending expression:
M
this is an object of type constr_under_binders
*)

Last updated: Jun 22 2024 at 16:02 UTC