The Coq mailing list

[Jean-Yves Vion-Dury <jean-yves.vion-dury AT inrialpes.fr>]

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   Research Scientist	Xerox Research Centre Europe
INRIA (sabbatical) 655 avenue de l'Europe, 38334 Montbonnot (FRANCE) 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 Circusthe Transformation Language I designed ?	show me