Basic
📁 Source: Batteries/Control/Nondet/Basic.lean
Statistics
| Metric | Count |
|---|---|
DefinitionsNondet, bind, filter, filterM, filterMap, filterMapM, firstM, head, instAlternativeMonad, instInhabited, instMonadLift, iterate, map, mapM, nil, ofList, ofListM, ofOption, ofOptionM, singleton, singletonM, squash, toList, toList', toMLList, toMLList', instMonadBacktrackUnitId_batteries | 27 |
| Theorems | 0 |
| Total | 27 |
Nondet
Definitions
| Name | Category | Theorems |
|---|---|---|
bind 📖 | CompOp | — |
filter 📖 | CompOp | — |
filterM 📖 | CompOp | — |
filterMap 📖 | CompOp | — |
filterMapM 📖 | CompOp | — |
firstM 📖 | CompOp | — |
head 📖 | CompOp | — |
instAlternativeMonad 📖 | CompOp | — |
instInhabited 📖 | CompOp | — |
instMonadLift 📖 | CompOp | — |
iterate 📖 | CompOp | — |
map 📖 | CompOp | — |
mapM 📖 | CompOp | — |
nil 📖 | CompOp | — |
ofList 📖 | CompOp | — |
ofListM 📖 | CompOp | — |
ofOption 📖 | CompOp | — |
ofOptionM 📖 | CompOp | — |
singleton 📖 | CompOp | — |
singletonM 📖 | CompOp | — |
squash 📖 | CompOp | — |
toList 📖 | CompOp | — |
toList' 📖 | CompOp | — |
toMLList 📖 | CompOp | — |
toMLList' 📖 | CompOp | — |
(root)
Definitions
| Name | Category | Theorems |
|---|---|---|
Nondet 📖 | CompData | — |
instMonadBacktrackUnitId_batteries 📖 | CompOp | — |
---