... | ... | @@ -160,6 +160,7 @@ theories/base_logic/lib is for constructions in the base logic (using own) |
|
|
theorem)
|
|
|
* 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.
|
|
|
|
|
|
### Naming algebra libraries
|
|
|
|
... | ... | |