Ssreflect Users Discussion List

[François Pottier <>]

Le 02/18/2016 11:30 AM, Benjamin Werner a écrit :
> If I recall correctly, the idea is to have a bunch of simple equality
> lemmas of the form forall x y, x+y = (x+y)%nat
> to apply them, and then call omega.

Thanks for this example. By the way, is autorewrite still used/useful 
under ssreflect? In standard Coq it would be the preferred way of 
applying a large set of rewriting rules until a normal form is reached.

--
François Pottier

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