The Coq mailing list

[Eduardo Gimenez <Eduardo.Gimenez AT trusted-logic.fr>]

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 
----------------------------------------------------------