The Coq mailing list

[Houda Anoun <anoun AT labri.fr>]

Hi,
The term "rx+ry=ry+rx" is not the beta contraction of (Rplus_comm rx ry) 
but its type....
In other terms (Rplus_comm rx ry) is a proof of (rx+ry=ry+rx)....
The term (Rplus_comm rx ry) ->  True is not well formed  (because  (Rplus_comm rx ry) 's type is not a 
sort ...,
that is the case for example for nat -> nat which is well formed  and 0 
-> nat which is not... 0:nat !!)
Hope this helps

Houda

> Dear colleagues
>
> I cannot understand for instance why
>
> Require Import Reals.
> Check forall rx ry:R, (Rplus_comm rx ry) -> True.
>
> produces the error :
>
> Error: In environment
> rx : R
> ry : R
> the term "Rplus_comm rx ry" has type "rx + ry = ry + rx"
> which should be Set, Prop or Type.
>
> whereas
>
> Check forall rx ry:R, rx+ry = ry+rx -> True.
>
> produces
>
> forall rx ry : R, rx + ry = ry + rx -> True
>      : Prop
>
>
> but, to me, rx+ry=ry+rx is the beta-contraction of (Rplus_comm rx ry)
> and hence, the type should be convertible.
>
> any comment much appreciated.
>
> Jean-Yves
>
> --
> Jean-Yves Vion-Dury <http://wam.inrialpes.fr/people/index.en.html>   
> /Research Scientist/     * Xerox Research Centre Europe *
> *INRIA* (sabbatical)
> 655 avenue de l'Europe,
> 38334 Montbonnot (FRANCE)
> Jean-Yves.Vion-Dury AT inrialpes.fr 
> <mailto:Jean-Yves.Vion-Dury AT inrialpes.fr> from France:   0 4 76 61 53 83
> from abroad: +33 4 76 61 53 83
> you may have heard of *Circus*the Transformation Language I designed ? 
> show me <http://www.google.com/search?q=Circus-DTE&ie=UTF-8&oe=%0A=UTF-8>