Ssreflect Users Discussion List

[Cyril Cohen <>]

Hi Andrej,

Le 10/10/2012 15:59, Andrej Bauer a écrit :
> I personally believe that this
> would greatly benefit our project, as ssreflect-style of proof is much
> better suited for mathematics than pure Coq. And I bet ssreflect would
> also benefit from additional exposure.

Well, I full agree with you on that point and I'm currently working on 
this matter. In order to begin as quickly as possible, I started from a 
patched version of Coq v8.3 (with the patches that can be found in the 
Foundation repository) and I modified (in a very ugly way for now) the 
ssr1.4_v8.3 plugin to make it work in the univalent setting. I also 
converted the most basic ssr libraries and began to formalize the 
beginning of the foundation from it, in a ssreflect style (mainly to 
understand it).

I will make my early development available on github anytime now (even 
if I think it will not match your expectations since I work with coq 
v8.3 right now) ... As for the proper ssr library, Enrico's answer 
coincides with what I expected.

Best regards,
--
Cyril Cohen