... | ... | @@ -134,7 +134,7 @@ Lemma foo (very_long_name : has_a_very_long_type) |
|
|
|
|
|
For tests with output put `Check "theorem name in a string"` before it so that the output from different tests is separated.
|
|
|
|
|
|
For long `t; [t1 | t2 | t3]` split them like this, and indent by 2 spaces:
|
|
|
For long `t1; t2; t3` and `t; [t1 | t2 | t3]` split them like this, and indent by 2 spaces:
|
|
|
|
|
|
**Good:**
|
|
|
```coq
|
... | ... | @@ -144,6 +144,13 @@ t; |
|
|
|t3].
|
|
|
```
|
|
|
|
|
|
```coq
|
|
|
t;
|
|
|
t1;
|
|
|
t2.
|
|
|
```
|
|
|
|
|
|
|
|
|
**TODO:** Keep all `Require`, `Import` and `Export` at the top of the file.
|
|
|
|
|
|
|
... | ... | |