coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Gyesik Lee <gslee AT ropas.snu.ac.kr>
To: Adam Chlipala <adam AT chlipala.net>
Cc: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] About mutual recursion
Date: Tue, 12 Oct 2010 04:28:06 +0900
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:from:date :x-google-sender-auth:message-id:subject:to:cc:content-type :content-transfer-encoding; b=GAZ6p9KSkVfvvL2/tbyWCiE1M5/0csX/AYPxX+4NPwRscoDkEfowj8N0XVDC1ShERE 5ETG6QGSpfuLoOmvRjBQ8RHIi8/GbjuP+D85TbhnUvRIdiYObtiQ2+l+s0k3a8Kw9wXU fI8ndoyJ6c9/RmplnpzYITUxlIg/e99HZgygE=

> My suggestion was more along the lines of replacing the second definition
> by:
> Definition VarIn r := bVarIn r = true.

I see. Thanks.

[Coq-Club] About mutual recursion, Gyesik Lee
- Re: [Coq-Club] About mutual recursion, Adam Chlipala
  - Re: [Coq-Club] About mutual recursion, Gyesik Lee
    - Re: [Coq-Club] About mutual recursion, Adam Chlipala
      - Re: [Coq-Club] About mutual recursion, Gyesik Lee
        
        Re: [Coq-Club] About mutual recursion, Gyesik Lee
        
        Re: [Coq-Club] About mutual recursion, Adam Chlipala
        
        Re: [Coq-Club] About mutual recursion, Gyesik Lee
        
        Re: [Coq-Club] About mutual recursion, AUGER Cedric
- Re: [Coq-Club] About mutual recursion, Thorsten Altenkirch
- Re: [Coq-Club] (Not) About mutual recursion, Jean-Francois Monin
  - Re: [Coq-Club] (Not) About mutual recursion, Gyesik Lee