coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Eduardo Gimenez <Eduardo.Gimenez AT trusted-logic.fr>
- To: Guillaume Dufay <Guillaume.Dufay AT sophia.inria.fr>
- Cc: coq-club AT pauillac.inria.fr
- Subject: Re: Pattern-matching on a redefined constructor name
- Date: Thu, 18 May 2000 11:52:16 +0200
- Organization: Trusted Logic
Hi,
As the identifier is_true is not a constructor, Coq considers it as a
variable. The scope of this variable is the corresponding branch of the case
expression, so it hides the constant is_true that you have previously defined
Hence, your definition is actually equivalent to :
Definition foo := [b:bool]
Cases b of
x => true |
_ => false
end.
As x matches any term., the definition is the constant function
[b:bool]true.
Actually, Coq should warn the user about the fact that the last
branch (_ => false) is unreachable.
Cheers,
Eduardo.
Le jeu, 18 mai 2000, vous avez écrit :
> Hello,
>
> I'm having a weird problem with the strategie Cases.
> Hereafter a small example in Coq :
>
> Require Bool.
>
> Definition is_true := true.
>
> Definition foo := [b:bool]
> Cases b of
> is_true => true |
> _ => false
> end.
>
> Print is_true.
> Print foo.
>
>
>
>
> And the result is :
> > is_true = true
> > : bool
> > foo = [_:bool]true
> > : bool->bool
>
> No pattern-matching is done on the redefined constructor true.
> Is that a normal behaviour? Is there a way to avoid this?
>
>
> Thank you in advance. Regards,
>
>
> Guillaume Dufay
--
----------------------------------------------------------
Eduardo Gimenez Tel : (33) 1 30 97 25 13
Trusted Logic SA Std : (33) 1 30 97 25 00
5, rue du Bailliage Fax : (33) 1 30 97 25 19
78000 Versailles Web : www.trusted-logic.fr
----------------------------------------------------------
- Pattern-matching on a redefined constructor name, Guillaume Dufay
- Re: Pattern-matching on a redefined constructor name, Eduardo Gimenez
- Re: Pattern-matching on a redefined constructor name, Benjamin Werner
- Re: Pattern-matching on a redefined constructor name, Eduardo Gimenez
Archive powered by MhonArc 2.6.16.