This first of few posts on this topic (the next will be request for code review for stuff I wrote)
For most programming languages, there is good coding practices/patterns that developers should stick to,
(stuff that goes into the linting of any programming language).
Is there similar good/bad practices for Coq, I am looking at things that include stuff to avoid, stuff to adhere to, naming conventions (especially lemma naming conventions, I don't know a good strategy to pick good names for theorems, lemmas). Any thing in general that makes code more readable for coq in particular (aside from commenting the code).
bonus points for any coq linters.
thanks a lot, I will see the styles referenced in the paper, but the third document is almost the thing I am looking for as a starting point.
walker has marked this topic as resolved.
Note that what is an anti-pattern in one style can be a pattern in another. If you're relying heavily on a given set of libraries (MathComp, Iris, etc), it might be a good idea to try to emulate its style. From what I understand the standard library doesn't have much of a fixed style.
the Stdlib has multiple styles. Sometimes consistent across a subset of files.
Last updated: Jan 29 2023 at 01:02 UTC