Basic
📁 Source: Batteries/Data/HashMap/Basic.lean
Statistics
| Metric | Count |
|---|---|
DefinitionsLawfulHashable, contains, empty, erase, find!, find?, findD, findEntry?, fold, foldM, forM, inner, insert, insert', instEmptyCollection, instGetElemOptionTrue, instInhabited, isEmpty, mergeWith, mergeWithM, modify, numBuckets, ofList, ofListWith, size, toArray, toList, mkHashMap, findEntry?, ofListWith | 30 |
| Theorems | 0 |
| Total | 30 |
Batteries
Definitions
| Name | Category | Theorems |
|---|---|---|
mkHashMap 📖 | CompOp | — |
Batteries.HashMap
Definitions
| Name | Category | Theorems |
|---|---|---|
LawfulHashable 📖 | MathDef | — |
contains 📖 | CompOp | — |
empty 📖 | CompOp | — |
erase 📖 | CompOp | — |
find! 📖 | CompOp | — |
find? 📖 | CompOp | — |
findD 📖 | CompOp | — |
findEntry? 📖 | CompOp | — |
fold 📖 | CompOp | — |
foldM 📖 | CompOp | — |
forM 📖 | CompOp | — |
inner 📖 | CompOp | — |
insert 📖 | CompOp | — |
insert' 📖 | CompOp | — |
instEmptyCollection 📖 | CompOp | — |
instGetElemOptionTrue 📖 | CompOp | — |
instInhabited 📖 | CompOp | — |
isEmpty 📖 | CompOp | — |
mergeWith 📖 | CompOp | — |
mergeWithM 📖 | CompOp | — |
modify 📖 | CompOp | — |
numBuckets 📖 | CompOp | — |
ofList 📖 | CompOp | — |
ofListWith 📖 | CompOp | — |
size 📖 | CompOp | — |
toArray 📖 | CompOp | — |
toList 📖 | CompOp | — |
Std.HashMap
Definitions
| Name | Category | Theorems |
|---|---|---|
findEntry? 📖 | CompOp | — |
ofListWith 📖 | CompOp | — |
---