Hi in the following reproducible example I get the error
"struct" annotation is expected.
I don't know what Ltac expects exactly, how would you match on a fixpoint like that?
Definition foo : nat -> Prop :=
fix F n :=
match n with
| 0 => True
| S n => False /\ F n
end.
Goal forall n, ~ foo (S n).
intros.
intro CONTRA.
unfold foo in CONTRA.
Fail match type of CONTRA with
| context[((fix F : nat -> Prop := _) ?n)] => idtac F
end.
Admitted.
fix
(and Fixpoint
) maintain the information of which argument they are structurally recursive on through a {struct n}
clause, and that's what Ltac seems to be asking you :
match type of CONTRA with
| context[((fix F (x : nat) {struct x} : Prop := _) ?n)] => idtac F
end.
Yes, that's exactly right. Thanks!
Last updated: Oct 13 2024 at 01:02 UTC