coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] strange behaviour while defining inductive types.

From: Pierre Courtieu <Pierre.Courtieu AT cnam.fr>
To: AUGER Cedric <Cedric.Auger AT lri.fr>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] strange behaviour while defining inductive types.
Date: Thu, 26 May 2011 12:18:22 +0200
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=B4+lpQOnpiixK4XfsJ9YTdnWEHP0OPy2dCb7njgh5zZyB0Qg2/tJ0cMJ+77xogbIft ZkQdpNzmGLFlvSgELA12+SaWc0we4E3RXMg9EDRWOP3IWyMBj7J3yMus/wQgck07Zmf4 E7pFwB3qalWRsLvON8NoQGQLYyGEgDsGrIX/g=

Strange indeed. Trying to understand how "if"s are compiled, I stumble
into something else: "Remove Printing If" command seems to be
ineffective (8.3pl1 and trunk):

Print Table Printing If. (* bool is there*)
Remove Printing If bool.
Print Table Printing If. (* bool is removed*)
Print bool_comp. (* still uses "if" *)
Set Printing All. (* let's try this *)
Print bool_comp. (* still uses "if" *)

P.

2011/5/26 AUGER Cedric
<Cedric.Auger AT lri.fr>:
> Hi all, I don't understand why the first definition is accepted and not
> the second one.
>
> Inductive bool_comp (b: bool): bool -> Prop :=
> | Opp: forall q, (if b
> � � � � � � � � then match q with true => False | false => True end
> � � � � � � � � else match q with true => True | false => False end)
> � � � � � � � � -> bool_comp b q.
>
> Print bool_comp.
> Inductive bool_comp2 (b: bool): bool -> Prop :=
> | Opp2: forall q, (match b return Prop with
> � � � � � � � � | true => match q return Prop with true => False |
> false => True end | false => match q return Prop with true => True |
> false => False end end) -> bool_comp2 b q.
>

[Coq-Club] strange behaviour while defining inductive types., AUGER Cedric
- Re: [Coq-Club] strange behaviour while defining inductive types., AUGER Cedric
- Re: [Coq-Club] strange behaviour while defining inductive types., Pierre Courtieu
- Re: [Coq-Club] strange behaviour while defining inductive types., Hugo Herbelin