Stream: Coq users

Topic: Request for Comments/ Code review

view this post on Zulip walker (Nov 01 2022 at 14:17):


So I was implementing the Extentional tries by Xavier Leroy (also I checked his implementation) but this time I was aiming to have a robust implementation (API-wise) so I kind of followed the approach taken by coq-stdpp except for I tried to use ssreflection as much as possible.

What I am asking for is general code review, maybe if you can see some bad patterns, ways to write shorter and better proofs, or maybe
even some misuses of ssreflect/mathcomp on my end.

The point here is that to be able to improve I need feedback on what may I be doing wrong (even from guidelines perspective)

The codebase is still at very early stage and very few lemmas / APIs, which will also make it easier to fix any bad coq habits I ended up developing.

view this post on Zulip Notification Bot (Nov 01 2022 at 16:41):

This topic was moved to #math-comp users > Request for Comments/ Code review by Karl Palmskog.

Last updated: Feb 09 2023 at 00:03 UTC