... | ... | @@ -38,6 +38,10 @@ Use `Lemma`, not `Theorem` (or the other variants: `Fact`, `Corollary`, |
|
|
|
|
|
We prefer `first [ t1 | fail 1 "..." ]` to `t1 || fail "..."` because the latter will fail if `t1` doesn't make progress. See https://gitlab.mpi-sws.org/iris/iris/-/issues/216. Note that `first [ t1 | fail "..."]` is simply incorrect; the failure message will never show up and will be replaced with a generic failure.
|
|
|
|
|
|
### Coqdoc comments
|
|
|
|
|
|
Module-level comments (covering the entire file) go at the top of the file, before the `Require`.
|
|
|
|
|
|
### Uncategorized
|
|
|
|
|
|
Indent the body of a match by one space:
|
... | ... | |