EStateM
📁 Source: Batteries/Lean/EStateM.lean
Statistics
| Metric | Count |
|---|---|
Definitionsmap | 1 |
Theoremsmap_eq_error, map_eq_ok, map_error, map_ok, dummyRestore_apply, dummySave_apply, ext, ext_iff, run'_adaptExcept, run'_bind, run'_fromStateM, run'_get, run'_getModify, run'_map, run'_modify, run'_modifyGet, run'_orElse, run'_pure, run'_seq, run'_seqLeft, run'_seqRight, run'_set, run'_throw, run'_tryCatch, run'_tryFinally', run_adaptExcept, run_bind, run_fromStateM, run_getModify, run_map, run_orElse, run_seq, run_seqLeft, run_seqRight, run_tryCatch, run_tryFinally' | 36 |
| Total | 37 |
EStateM
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
dummyRestore_apply 📖 | — | — | — | — | — |
dummySave_apply 📖 | — | — | — | — | — |
ext 📖 | — | — | — | — | — |
ext_iff 📖 | — | — | — | — | ext |
run'_adaptExcept 📖 | — | — | — | — | run'.eq_1run_adaptExcept |
run'_bind 📖 | — | — | — | — | run'.eq_1run_bind |
run'_fromStateM 📖 | — | — | — | — | — |
run'_get 📖 | — | — | — | — | — |
run'_getModify 📖 | — | — | — | — | — |
run'_map 📖 | — | — | — | — | run'.eq_1run_map |
run'_modify 📖 | — | — | — | — | — |
run'_modifyGet 📖 | — | — | — | — | — |
run'_orElse 📖 | — | — | — | — | run'.eq_1run_orElse |
run'_pure 📖 | — | — | — | — | — |
run'_seq 📖 | — | — | — | — | run'_bindrun'_map |
run'_seqLeft 📖 | — | — | — | — | run'_bindrun'_map |
run'_seqRight 📖 | — | — | — | — | run'.eq_1run_seqRight |
run'_set 📖 | — | — | — | — | — |
run'_throw 📖 | — | — | — | — | — |
run'_tryCatch 📖 | — | — | — | — | run'.eq_1run_tryCatch |
run'_tryFinally' 📖 | — | — | — | — | — |
run_adaptExcept 📖 | — | — | — | — | — |
run_bind 📖 | — | — | — | — | — |
run_fromStateM 📖 | — | — | — | — | — |
run_getModify 📖 | — | — | — | — | — |
run_map 📖 | mathematical | — | Result.map | — | — |
run_orElse 📖 | — | — | — | — | — |
run_seq 📖 | — | — | — | — | — |
run_seqLeft 📖 | — | — | — | — | — |
run_seqRight 📖 | — | — | — | — | — |
run_tryCatch 📖 | — | — | — | — | — |
run_tryFinally' 📖 | — | — | — | — | — |
EStateM.Result
Definitions
| Name | Category | Theorems |
|---|---|---|
map 📖 | CompOp |
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
map_eq_error 📖 | mathematical | — | map | — | — |
map_eq_ok 📖 | mathematical | — | map | — | — |
map_error 📖 | mathematical | — | map | — | — |
map_ok 📖 | mathematical | — | map | — | — |
---