... | ... | @@ -130,6 +130,23 @@ Lemma foo (very_long_name : has_a_very_long_type) |
|
|
x < y → y < z → x < z.
|
|
|
```
|
|
|
|
|
|
For definitions that don't fit into one line, put `:=` before the linebreak, not after.
|
|
|
|
|
|
|
|
|
**Bad:**
|
|
|
|
|
|
```coq
|
|
|
Definition foo (arg1 arg2 arg3 : name_of_the_type)
|
|
|
:= the body that is very long.
|
|
|
```
|
|
|
|
|
|
**Good:**
|
|
|
|
|
|
```coq
|
|
|
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.
|
... | ... | |