Ssreflect Users Discussion List

[Cyril Cohen <>]

Hello Frédéric,

First, you should know that you are currently playing with non released (yet)
features of the ssreflect library, and I thank you for this feedback.

On 27/03/2012 23:30, Frédéric Chyzak wrote:
> I find it counter-intuitive that positive and negative numbers get 
> displayed in 
> so different ways.  If Negz cannot be avoided, I wonder if I would not 
> prefer 
> seeing the Posz for non-negative integers (despite the misnomer).  What is 
> the 
> rationale?
> 
> Or, is there a way to get a more "traditional" display (with minus signs)?

I agree this is disturbing, however, (Negz _) is not to be used, one should
prefer form (- _%:Z). Negz can accidentally occur while doing a proof, e.g.
because you did a "case: x" instead of "case: (intP x)". But then one may use 
the
rewriting rule NegzE to replace (Negz n) by (- n.+1%:Z). In fact, these two 
last
terms are convertible.

Maybe the documentation can be improved to reflect these recommandations.

Best,
-- 
Cyril Cohen