... | ... | @@ -165,6 +165,13 @@ theories/base_logic/lib is for constructions in the base logic (using own) |
|
|
* Suffix `'` (prime) is used when `foo'` is a corollary of `foo`. Try to avoid
|
|
|
these since the name doesn't convey how `foo'` is related to `foo`.
|
|
|
* Given a polymorphic function/relation `f` (e.g., `eq`, `equiv`, `subseteq`), the instance of type `A` is called `A_f_instance`, and we add a lemma `A_f` that characterizes the instance. In case of many instances, this lemma is proved by unfolding the definition of the instance, e.g., `frac_op`, `frac_valid`. However, in some cases, e.g., `list_eq`, `map_eq`, `set_eq` this lemma might require non-trivial proof work.
|
|
|
* For lemmas involving modalities, we usually follow this naming scheme:
|
|
|
```
|
|
|
M1_into_M2: M1 P ⊢ M2 P
|
|
|
M1_M2_elim: M1 (M2 P) ⊣⊢ M1 P
|
|
|
M1_elim_M2: M1 (M2 P) ⊣⊢ M2 P
|
|
|
M1_M2: M1 (M2 P) ⊣⊢ M2 (M1 P)
|
|
|
```
|
|
|
|
|
|
### Naming algebra libraries
|
|
|
|
... | ... | @@ -189,4 +196,4 @@ theories/base_logic/lib is for constructions in the base logic (using own) |
|
|
* `φ` and `ψ` for `Prop`
|
|
|
* `A` `B` for types, ofeT, or cmraT
|
|
|
|
|
|
Suffixes like O, R, UR (already documented) |
|
|
Suffixes like O, R, UR (already documented) |
|
|
\ No newline at end of file |