Ssreflect Users Discussion List

[Cyril Cohen <>]

On 01/12/2014 01:34, Arthur Azevedo de Amorim wrote:
> Goal [forall b : bool, b == (0 < (b : nat))].

Hi, in this particular instance "by do ?[rewrite unlock|compute]." would
do the trick.

However, for general purpose (and in case of the need to change
algorithms and data representation) we (Maxime Dénès, Anders Mörtberg
and I) started a library named CoqEAL [1] which goal is to translate
automatically such statement in computable (and if possible efficiently)
counterparts.

Best,
-- 
Cyril Cohen
[1] https://github.com/CoqEAL/CoqEAL