Ssreflect Users Discussion List

[Enrico Tassi <>]

On Wed, Oct 10, 2012 at 10:54:47AM -0400, Andrej Bauer wrote:
> To answer Assia's question: yes, the HoTT library does not use the
> standard library because we redefine equality (or to put it better, it
> does not land in Prop). So we want to be careful about putting things
> back in, but we will of course put back in anything that is ok with
> the new interpretation. I was forced to get rid of the standard
> library because it would not compile at all with the new
> interpretation of inductive types. I don't think there is anything
> problematic in Bool.v.

Ah OK, not it makes much more sense and looks way more feasible ;-)

And maybe with some coordination we could avoid doing the work 3 times,
and sime I'm not in Princeton I guess I should let Assia (and Cyril) take
the leed.
I can surely help on the .ml4 side, if something needs to be adapted.

Cheers
-- 
Enrico Tassi