Hello, I noticed that the algorithms in FMapTwoThreeK have no proofs attached. Is this beggin for volunteers or is the prevailing opinion that proofs are not needed for this part of the code (and what would be the reason)?
Is this beggin for volunteers
That looks like it to me.
Volunteers would we great.
This topic was moved by Théo Zimmermann to #Coq Platform devs & users > coq-ext-lib
Last updated: Jun 03 2023 at 18:01 UTC