Does Coq have an established convention/style for constructors, variables, terms, &c?
An established convention that isn't exceptionless is totally fine. For example, terms should be lowercase like
nat unless you're trying to mimic math notation in cases like
Z is a good convention.
The naming convention I've started using for toy Coq code is
PascalCase for variables and constructors and
snake_case for everything else.
I like being able to visually distinguish variables and nonvariables at a glance, and like naming single-argument constructors after the type of their argument, which is possible in this convention.
However, using the same portion of the namespace for constructors and variables leads to problems.
In this code snippet,
MisspelledConstructor is a variable and will unify with anything. This problem is not huge is practice because Coq enforces exhaustiveness in match statements, but distinguishing constructors and variables by convention would lead to more informative error messages and make debugging slightly easier.
match thing with | MisspelledConstructor => expression | (* some pattern *) => (* this expression is unreachable because MisspelledConstructor matches everything *) end