coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] About mutual recursion

From: Gyesik Lee <gslee AT ropas.snu.ac.kr>
To: Adam Chlipala <adam AT chlipala.net>, Thorsten Altenkirch <txa AT cs.nott.ac.uk>
Cc: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] About mutual recursion
Date: Tue, 12 Oct 2010 03:04:09 +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; b=BfG4JtLFcLixhRbhAh3wSC071/irTdoCjk2Kge9PngZfgWMoZVgm7aj59349p//YCI Z0BWl7xeCzCHfdn2gOXqUQap+lB/tfdpFmoUqsjjrokY8SvIbfHIuaXrSUiVZkR+ZhUW FLxvLoTVHpO5227mDlCmm3xxG5WLH2UnlsW2c=

> Why don't you just use [bool] instead of [Prop]?
>

because I want to have the property that there is no term of type
[VarIn r] when its value is False.
But this does not work with the Boolean [false].

Gyesik

[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