0963f3476c
This makes changes to the `GetElem` class so that it does not lead to unnecessary overhead in container like `RBMap`. The changes are to: 1. Make `getElem?` and `getElem!` part of the `GetElem` class so they can be overridden in instances. 2. Introduce a `LawfulGetElem` class that contains correctness theorems for `getElem?` and `getElem!` using the original definitions. 3. Reorganize definitions (e.g, by moving `GetElem` out of `Init.Prelude`) so that the `GetElem` changes are feasible. 4. Provide `LawfulGetElem` instances to complement all existing `GetElem` instances in Lean core. To reduce the size of the PR, this doesn't do the work of providing new `GetElem` instances for `RBMap`, `HashMap` etc. That will be done in a separate PR (#3688) that depends on this. --------- Co-authored-by: Mac Malone <tydeu@hatpress.net> |
||
|---|---|---|
| .. | ||
| Basic.lean | ||