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:
This script could be a start:
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.
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: Feb 06 2023 at 06:29 UTC