This PR replaces the existing implementations of `(D)HashMap.alter` and `(D)HashMap.modify` with primitive, more efficient ones and in particular provides proofs that they yield well-formed hash maps (`WF` typeclass). --------- Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com> |
||
|---|---|---|
| .. | ||
| AdditionalOperations.lean | ||
| Basic.lean | ||
| Lemmas.lean | ||
| Raw.lean | ||
| RawLemmas.lean | ||