... | ... | @@ -32,10 +32,6 @@ Use `Context`, never `Variable` |
|
|
Use `Lemma`, not `Theorem` (or the other variants: `Fact`, `Corollary`,
|
|
|
`Remark`)
|
|
|
|
|
|
Tests may use `Example` for theorems.
|
|
|
|
|
|
*RJ*: Why this? In Iris itself, they use `Lemma` as well.
|
|
|
|
|
|
### Uncategorized
|
|
|
|
|
|
Indent the body of a match by one space:
|
... | ... | @@ -49,6 +45,8 @@ match foo with |
|
|
|
|
|
*RJ*: This is odd, usually everything is in (multiples of) 2 spaces, I think.
|
|
|
|
|
|
*Tej*: https://gitlab.mpi-sws.org/iris/iris/-/blob/920bc3d97b8830139045e1780f2aff4d05b910cd/iris_heap_lang/proofmode.v#L194
|
|
|
|
|
|
Avoid using the extra square brackets around an Ltac match:
|
|
|
|
|
|
**Good:**
|
... | ... | @@ -124,8 +122,6 @@ Lemma foo (very_long_name : has_a_very_long_type) |
|
|
|
|
|
**TODO:** Use `"[H1 H2]"` when possible otherwise do `"(H1 & H2 & H3)"`
|
|
|
|
|
|
*RJ*: I added spaces around the `&`.
|
|
|
|
|
|
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:
|
... | ... | |