coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Re: recursive Ltac definitions

From: Aaron Bohannon <bohannon AT cis.upenn.edu>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] Re: recursive Ltac definitions
Date: Wed, 20 Oct 2010 13:09:03 -0400
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:date :x-google-sender-auth:message-id:subject:from:to:content-type :content-transfer-encoding; b=tBnV2SaRHLneCaNqGcgu6C881f7HaPfAhrgJVp9VtPecYha5bmrwnh2aOtWqbpJA8K 3v545qFnqGSr4HQr8eXA7LbwA2IKIVSRuYg0GJOHJmfmgLg0CIQ1IGThCRf4TUOQlgGg 5PAbMofxCPmSiUdCkdi9r1zCixXkFURegaU3Y=

a-ha! It's a parsing problem.

- Aaron

On Wed, Oct 20, 2010 at 12:48 PM, Aaron Bohannon
<bohannon AT cis.upenn.edu>
wrote:
> Why do the first four definitions succeed while the fifth one fails?
> (I have a very hard time imagining I'm the first to discover this...)
>
> Ltac t := t.
>
> Ltac t := t t.
>
> Ltac t u := t u.
>
> Ltac t u := t t u.
>
> Ltac t u := t (t u).
> Error: The reference t was not found in the current environment.
>
> �- Aaron
>

[Coq-Club] recursive Ltac definitions, Aaron Bohannon
- [Coq-Club] Re: recursive Ltac definitions, Aaron Bohannon
  - [Coq-Club] Equational Reasoning over streams, Herman Geuvers
    - Re: [Coq-Club] Equational Reasoning over streams, Thorsten Altenkirch
      - Re: [Coq-Club] Equational Reasoning over streams, David Leduc
        
        Re: [Coq-Club] Equational Reasoning over streams, Herman Geuvers
        
        Re: [Coq-Club] Equational Reasoning over streams, AUGER Cedric
        
        Re: [Coq-Club] Equational Reasoning over streams, Keiko Nakata
        
        Re: [Coq-Club] Equational Reasoning over streams, David Leduc
- Re: [Coq-Club] recursive Ltac definitions, Adam Chlipala