Consider consistency for the exercises

[kytrinyx]

• Is there a style guide for Coq?
• Are these styles encouraged or enforced?
• Are there any conventions that we should adopt on this track for the sake of consistency?
• Can we enforce these?
• Is there a linter? Are there many? Should we use one?
• When you add a linter, edit the pull request template [link]
• Update the pull request template with checks that are appropriate for this track
• Is there a common convention for filenames? If not, what should our convention be?

Note that this is about the exercises (the test suites and code examples), not people's solutions.

[bagnalla]

Here are my thoughts on this.

• AFAIK there isn't much of a style guide beyond a few simple things listed here: https://coq.inria.fr/cocorico/CoqStyle. Some people (e.g., Adam Chlipala in his book "Certified Programming with Dependent Types") advocate automating proof scripts as much as possible by writing a lot of custom Ltac, but that's more about development methodology than style.
• Encouraged.
• Probably at least the things described in the link above.
• No linter that I'm aware of.
• In the Coq projects I've contributed to, the files are all lower case with no underscores or anything. However, the files provided for the "Software Foundations" textbook (a popular book for learning Coq) all begin with a capital letter.