coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Houda Anoun <anoun AT labri.fr>
- To: Dan Synek <synek AT cs.kun.nl>
- Cc: Coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] recursive ltacs
- Date: Tue, 14 Sep 2004 10:35:38 +0200
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Hi,
I think that the expression (and (Ct f1) (Ct f2)) is not a well formed one as it is not allowed by the grammar of the language Ltac. (cf. Coq Manual page 168 for more details about the syntax of Ltac)
Otherwise, we can easily write recursive tactics for example the following one:
Ltac Ct F :=
match F with
true => True
| false => False
| (andb ?f1 ?f2) => (Ct f1)
end.
In your case why do you want to define a tactic? and not a recursive function ?
Hope it helps
Houda
Dan Synek wrote:
Hi,
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?
Thanks
Dan
--------------------------------------------------------
Bug reports: http://coq.inria.fr/bin/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
--
==============================
| Houda ANOUN |
| LaBRI |
| 351 Cours de la libération |
| 33405 Talence |
| phone: 0540002489 |
:anoun AT labri.fr
|
=============================
- [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.