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: 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




Archive powered by MhonArc 2.6.16.

Top of Page