coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Hugo Herbelin <herbelin AT pauillac.inria.fr>
- To: synek AT cs.kun.nl (Dan Synek)
- Cc: Coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] recursive ltacs
- Date: Tue, 14 Sep 2004 10:37:56 +0200 (MET DST)
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Hi Dan,
> This is a part of a tactic I want to wtite:
>
> Ltac Ct F :=
> match F with
> true => True
> | false => False
> | (andb ?f1 ?f2) => and (Ct f1) (Ct f2)
> end.
> I get the following error message:
> Error: The reference Ct was not found in the current environment
> It seems like Coq does not allow recursive tactics, but according to
> the manual it does.
> What am I doing wrong?
This is because Ltac subexpressions (to the exception of variables)
are not allowed as part of Coq term expressions. You have to use
"let"'s as follows:
Ltac Ct F :=
match F with
true => True
| false => False
| (andb ?f1 ?f2) => let c1 := Ct f1 with c2 := Ct f2 in constr:(and c1 c2)
end.
Best regards,
Hugo
- [Coq-Club] recursive ltacs, Dan Synek
- Re: [Coq-Club] recursive ltacs, Houda Anoun
- Re: [Coq-Club] recursive ltacs, Hugo Herbelin
- Re: [Coq-Club] recursive ltacs,
Jasper Stein
- Re: [Coq-Club] recursive ltacs, Hugo Herbelin
- Re: [Coq-Club] recursive ltacs, Hugo Herbelin
- Re: [Coq-Club] recursive ltacs,
Jasper Stein
Archive powered by MhonArc 2.6.16.