I had hoped that stdlib2 would provide more guiding principles and more core for people to build on. I haven't followed closely enough

There does not seem to be too much progress on stdlib2.

Considering the previous discussion about coding conventions. It should be possible to write linter for this:

https://github.com/coq/stdlib2/blob/master/CONTRIBUTING.md

This script could be a start:

http://www.eelis.net/coqindent/

https://sympa.inria.fr/sympa/arc/coq-club/2009-11/msg00074.html

This topic was moved here from #Coq Platform devs & users > coq-ext-lib by Théo Zimmermann

I'm thinking less about naming and notation and more about core abstractions, e.g. `Monad`

, `Monoid`

, etc. Both ExtLib and stdpp define `Monad`

, some form of `decide`

, finite maps, etc in different ways and that basically means that there's no way to interface those two components. If there was a canonical definition that we could get behind, then we wouldn't need to worry so much about re-inventing each wheel :-) I probably contributed to this problem with the definitions in ExtLib because, I will admit, that I did not look closely at your past work at the time. I would be very eager to remedy this (though there are obviously time constraints on my side and the sides of other interested parties).

Last updated: Jun 22 2024 at 23:01 UTC