Ssreflect Users Discussion List

[Arthur Azevedo de Amorim <>]

Hi Cyril,

Thanks for your idea, I hadn't thought about using compute indeed.

I've been meaning to try CoqEAL for some time, indeed (I was just
reading the paper). I might have a use for it very soon, actually :)

Best


2014-11-30 23:48 GMT-05:00 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
>



-- 
Arthur Azevedo de Amorim