This PR optimizes the proofs in the internal file `Std/Data/DHashMap/Internal/RawLemmas.lean` so that the file is quicker to elaborate. |
||
|---|---|---|
| .. | ||
| AssocList | ||
| List | ||
| Defs.lean | ||
| Index.lean | ||
| Model.lean | ||
| Raw.lean | ||
| RawLemmas.lean | ||
| WF.lean | ||
This PR optimizes the proofs in the internal file `Std/Data/DHashMap/Internal/RawLemmas.lean` so that the file is quicker to elaborate. |
||
|---|---|---|
| .. | ||
| AssocList | ||
| List | ||
| Defs.lean | ||
| Index.lean | ||
| Model.lean | ||
| Raw.lean | ||
| RawLemmas.lean | ||
| WF.lean | ||