... | ... | @@ -188,16 +188,10 @@ 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.
|
|
|
## Parameter order and implicitness for lemmas
|
|
|
|
|
|
* Parameter order is usually from more higher-order to less higher-order (types, functions, plain values), and otherwise follows the order in which variables appear in the lemma statement.
|
|
|
* In new lemmas, arguments should be marked as implicit when they can be inferred by unification in all intended usage scenarios. (If an argument can *sometimes* be inferred, we do not have a clear guideline yet -- consider on a case-by-case basis, for now.)
|
|
|
|
|
|
## Metavariables
|
|
|
**TODO:** move these to the right place
|
... | ... | |