... | ... | @@ -79,7 +79,7 @@ Proof. split. |
|
|
Qed.
|
|
|
```
|
|
|
|
|
|
Put the entire theorem statement on one line or one premise per line.
|
|
|
Put the entire theorem statement on one line or one premise per line, indented by 2 spaces.
|
|
|
|
|
|
**Bad:**
|
|
|
|
... | ... | @@ -99,9 +99,27 @@ Lemma foo x y z : x < y → y < z → x < z. |
|
|
|
|
|
```coq
|
|
|
Lemma foo x y z :
|
|
|
x < y →
|
|
|
y < z →
|
|
|
x < z.
|
|
|
x < y →
|
|
|
y < z →
|
|
|
x < z.
|
|
|
```
|
|
|
|
|
|
If the parameters before the `:` become too long, indent later lines by 4 spaces and always have a newline after `:`:
|
|
|
|
|
|
**Bad:**
|
|
|
|
|
|
```coq
|
|
|
Lemma foo (very_long_name : has_a_very_long_type)
|
|
|
(even_longer_name : has_an_even_longer_type) : x < y → y < z →
|
|
|
x < z.
|
|
|
```
|
|
|
|
|
|
**Good:**
|
|
|
|
|
|
```coq
|
|
|
Lemma foo (very_long_name : has_a_very_long_type)
|
|
|
(even_longer_name : has_an_even_longer_type) :
|
|
|
x < y → y < z → x < z.
|
|
|
```
|
|
|
|
|
|
**TODO:** Use `"[H1 H2]"` when possible otherwise do `"(H1 & H2 & H3)"`
|
... | ... | |