Ssreflect Users Discussion List

[François Pottier <>]

Hi Georges,

Le 02/18/2016 11:57 AM, Georges Gonthier a écrit :
> So, rewriting with H means replacing m <= n with true.

Thanks for pointing this out...

> We’d need to introduce a synonym to support monotone rewriting,

Could you expand on what you have in mind? Do you mean that one should
introduce a synonym for "m <= n"? Would this approach be essentially
equivalent to 1- replacing "m <= n" with "le m n" everywhere; 2- using
setoid rewrite on the relation le; 3- performing step 1- in reverse?

--
François Pottier

http://gallium.inria.fr/~fpottier/