Ssreflect Users Discussion List

[Cyril Cohen <>]

On 01/12/2014 12:04, Cyril Cohen wrote:
> 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.

PS: Sadly, our work only covers a small part of algorthims in linear
algebra for now, so we do not provide yet tools to translate
quantifications on finite types.

-- 
Cyril Cohen