stdlib2
stdlib2 copied to clipboard
coq
Universes
This discussion is bound to happen at some point, so we might just as well start a new thread now, with this quote from @Hustmphrrr on Coq-Club: >I am not...
Opening a discusison: I am not sure this is in the scope of stdlib2 or if this is already thought of, but it would be nice to move all default...
User developments often use stdlib functions with inputs whose natural equivalence relation does not coincide with `Logc.eq`: most importantly functions, but also `Q`, non-`hprop` sigma types, etc. Then they eventually...
A gitter discussion suggested making stdlib2 compatible with [stdpp](https://gitlab.mpi-sws.org/iris/stdpp). Is that a realistic goal? @robbertkrebbers @RalfJung
Since Stdlib2 will also mean rethinking the hint databases, what about setting the [`Loose Hint Behavior`](https://coq.inria.fr/refman/proof-engine/tactics.html#coq:opt.loose-hint-behavior-lax-warn-strict) option to "Strict"? cc coq/coq#7710
First of all, I'm excited about this effort. As a new Coq user, it can be very difficult to figure out which aspects of the standard library reflect current best...
There are a lot of finite map and finite set implementations out there and I think it would be good to discuss what the shape of these types should be...
Here is some lore about abstraction and modularity mechanisms in Coq and Lean which I think may be relevant for setting conventions for stdlib2: - example of where module functors...
Many people are eager to contribute to the stdlib2 project so it would be very useful if a more specific roadmap could be shared and regularly updated, and it should...
In addition to the important question of what goes in the prelude, another question is: "What goes in the library?" Is there a list somewhere of the functionality we will...
