Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] recursive ltacs

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] recursive ltacs


chronological Thread 
  • 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       |
|  e-mail 
:anoun AT labri.fr
    |
=============================







Archive powered by MhonArc 2.6.16.

Top of Page