Coq doesn't have an official style guide.
This is an attempt to write down the style that I follow while
writing Coq code.
- Type annotations: Use
value: Type format
- Note: Coq standard library seems to favour
value : Type, which is in line with Agda.
- Indendation: 2 spaces per level. Don't use tab.
- All imports should appear at the top of the file
- All
Reserved Notation lines should appear on top of the
file, after the imports
- Constructor names should start with uppercase
- Type names should start with lowercase.
- Module names should start with uppercase.
- Use
Context instead of Variable for
sections
Suggestions:
- If there are more than 2 related notations, consider making a
separate module just for them with its own scope.
- The module name should end with
Notations.
- Eg:
RegexNotations
- Try to