This is a collaborative pull request to gather tips and good practices for writing Coq code.
It addresses casual but regular Coq users but not power users and aims to gather mostly uniformly accepted good practices.
If you would like to contribute, to facilitate collaboration, we recommend using github's code suggestions that ease reviewing and collaborative discussions. Alternatively, you can also make short PR to this one.
When suggesting tips, keep in mind they can be different solutions to a problem, so do not present something as "the solution" but "a solution" that comes with its advantages and inconvenient.
For instance, we all agree that we should not directly use variables named by Coq, but then there are different solutions that are not necessarily excluded:
always name your variables (ex: intros, as)
use tactics that do not require names like assumption
use tactics that do not introduce names like SSReflect's ones
For the moment, there is no fixed structure, but we could imagine sections like "tips for resilient code", "tips for efficiency" etc...
This is a collaborative pull request to gather tips and good practices for writing Coq code. It addresses casual but regular Coq users but not power users and aims to gather mostly uniformly accepted good practices.
If you would like to contribute, to facilitate collaboration, we recommend using github's code suggestions that ease reviewing and collaborative discussions. Alternatively, you can also make short PR to this one.
When suggesting tips, keep in mind they can be different solutions to a problem, so do not present something as "the solution" but "a solution" that comes with its advantages and inconvenient.
For instance, we all agree that we should not directly use variables named by Coq, but then there are different solutions that are not necessarily excluded:
intros,as)assumptionFor the moment, there is no fixed structure, but we could imagine sections like "tips for resilient code", "tips for efficiency" etc...