... | ... | @@ -130,7 +130,10 @@ theories/base_logic/lib is for constructions in the base logic (using own) |
|
|
* `list_lookup_insert` is named by context (the type involved), then the two functions outside-in on the left-hand-side, so it has the type `lookup (insert …) = …` where the `insert` is on a list. Notations mean it doesn’t actually look like this and the insert is textually first.
|
|
|
* Injectivity theorems are instances of `Inj` and then are used with `inj`
|
|
|
* Suffixes `_l` and `_r` when we have binary `op x y` and a theorem related to the left or right. For example, `sep_mono_l` says bi_sep is monotonic in its left argument (holding the right constant)
|
|
|
* Entailments at the top level are typically written P -* Q, which is notation for P ⊢ Q. If we have a theorem which has no premises you use ⊢ P explicitly (for example, common to have ⊢ |==> ∃ γ, … for an allocation theorem)
|
|
|
* Entailments at the top level are typically written `P -* Q`, which is notation
|
|
|
for P ⊢ Q. If you have a theorem which has no premises you have to write ⊢ P
|
|
|
explicitly (for example, common to have `⊢ |==> ∃ γ, …` for an allocation
|
|
|
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`.
|
|
|
|
... | ... | @@ -138,6 +141,17 @@ theories/base_logic/lib is for constructions in the base logic (using own) |
|
|
|
|
|
**TODO:** describe any conclusions we came to with the `mono_nat` library
|
|
|
|
|
|
## Parameter order for lemmas
|
|
|
|
|
|
* Update lemmas for ghost state should generally take the new value as the first
|
|
|
argument, since it cannot be inferred based on the premise so the user is
|
|
|
likely to supply it explicitly.
|
|
|
* **TODO:** what should general advice be on arguments the user might supply?
|
|
|
Make things implicit, or make it first? This is annoying to change later since
|
|
|
it's a breaking change, but hard to predict what typical usage will look like.
|
|
|
We might lean towards more implicits in general, since they're actually easier
|
|
|
to instantiate.
|
|
|
|
|
|
## Metavariables
|
|
|
**TODO:** move these to the right place
|
|
|
|
... | ... | |