Skip to content
Snippets Groups Projects
Verified Commit 8d61039e authored by Isaac van Bakel's avatar Isaac van Bakel
Browse files

Add style point on branching patterns

This style point came up in the feedback on #923, where a lack of
explicit branching in a pattern made a proof more confusing.

I've also moved another pattern-based style point into the newly-created
section just to take advantage of the increased organisation.
parent 1af9e5d6
No related branches found
No related tags found
No related merge requests found
......@@ -16,6 +16,32 @@ so we can add it.
This applies to Context, Implicit Types, and definitions
### Patterns
#### Disjunctions & branches
Always mark the disjuncts when destructuring a disjunctive pattern, even if you don't bind anything, to indicate that the proof branches
**Good:**
```coq
Lemma foo : b : bool, b = true b = false.
Proof.
intros [|].
...
```
**Bad:**
```coq
Lemma foo : b : bool, b = true b = false.
Proof.
intros [].
...
```
#### Uncategorized
**TODO:** Use `"[H1 H2]"` when possible otherwise do `"(H1 & H2 & H3)"`
### Unicode
Always use Unicode variants of forall, exists, ->, <=, >=
......@@ -147,8 +173,6 @@ Definition foo (arg1 arg2 arg3 : name_of_the_type) :=
the body that is very long.
```
**TODO:** Use `"[H1 H2]"` when possible otherwise do `"(H1 & H2 & H3)"`
For tests with output put `Check "theorem name in a string"` before it so that the output from different tests is separated.
For long `t1; t2; t3` and `t; [t1 | t2 | t3]` split them like this, and indent by 2 spaces:
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment