Ssreflect Users Discussion List

[Cyril Cohen <>]

Hi Erik,

Le 23/08/2013 12:09, Erik Martin-Dorel a écrit :
> It seems to me that lt/gt and le/ge should be permuted, because the
> current mapping of these notations is misleading.  For instance,

This behavior was intentional, the reason for it was that this notation is
dedicated to application to 0 or 1 arguments, and when you partially apply it
to one argument, it becomes confusing with OCaml conventions.
Indeed, I would naturally think that the predicate (<= 0) means "smaller than
0" (which is correct with the current ssr conventions) rather than "greater
than 0" (like in OCaml).
It seemed to me a good idea at the time, but I'm not sure anymore.

I'd like to know other user's point of view on the matter.

Cheers,
-- 
Cyril