SatisfiesM
📁 Source: Batteries/Classes/SatisfiesM.lean
Statistics
| Metric | Count |
|---|---|
DefinitionsMonadSatisfying, instEStateM, instExcept, instExceptT, instId, instOption, instReaderT, instStateRefT', instStateT | 9 |
Theoremsval_eq, bind, bind_pre, imp, map, mapConst, map_post, map_pre, of_true, pure, seq, seqLeft, seqRight, seq_post, seq_pre, seq_pre', trivial, SatisfiesM_EStateM_eq, SatisfiesM_ExceptT_eq, SatisfiesM_Except_eq, SatisfiesM_Id_eq, SatisfiesM_Option_eq, SatisfiesM_ReaderT_eq, SatisfiesM_StateRefT_eq, SatisfiesM_StateT_eq | 25 |
| Total | 34 |
MonadSatisfying
Definitions
| Name | Category | Theorems |
|---|---|---|
instEStateM 📖 | CompOp | — |
instExcept 📖 | CompOp | — |
instExceptT 📖 | CompOp | — |
instId 📖 | CompOp | — |
instOption 📖 | CompOp | — |
instReaderT 📖 | CompOp | — |
instStateRefT' 📖 | CompOp | — |
instStateT 📖 | CompOp | — |
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
val_eq 📖 | mathematical | SatisfiesM | satisfying | — | — |
SatisfiesM
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
bind 📖 | — | SatisfiesM | — | — | — |
bind_pre 📖 | — | SatisfiesM | — | — | bind |
imp 📖 | — | SatisfiesM | — | — | — |
map 📖 | — | SatisfiesM | — | — | — |
mapConst 📖 | — | SatisfiesM | — | — | map |
map_post 📖 | — | SatisfiesM | — | — | map |
map_pre 📖 | — | SatisfiesM | — | — | map |
of_true 📖 | mathematical | — | SatisfiesM | — | — |
pure 📖 | mathematical | — | SatisfiesM | — | — |
seq 📖 | — | SatisfiesM | — | — | — |
seqLeft 📖 | — | SatisfiesM | — | — | seq_premap |
seqRight 📖 | — | SatisfiesM | — | — | seq_premap |
seq_post 📖 | — | SatisfiesM | — | — | seq |
seq_pre 📖 | — | SatisfiesM | — | — | seq |
seq_pre' 📖 | — | SatisfiesM | — | — | seq |
trivial 📖 | mathematical | — | SatisfiesM | — | of_true |
(root)
Definitions
| Name | Category | Theorems |
|---|---|---|
MonadSatisfying 📖 | CompData | — |
Theorems
| Name | Kind | Assumes | Proves | Validates | Depends On |
|---|---|---|---|---|---|
SatisfiesM_EStateM_eq 📖 | mathematical | — | SatisfiesM | — | EStateM.extEStateM.run_mapEStateM.run.eq_1 |
SatisfiesM_ExceptT_eq 📖 | mathematical | — | SatisfiesM | — | — |
SatisfiesM_Except_eq 📖 | mathematical | — | SatisfiesM | — | — |
SatisfiesM_Id_eq 📖 | mathematical | — | SatisfiesM | — | — |
SatisfiesM_Option_eq 📖 | mathematical | — | SatisfiesM | — | — |
SatisfiesM_ReaderT_eq 📖 | mathematical | — | SatisfiesM | — | — |
SatisfiesM_StateRefT_eq 📖 | mathematical | — | SatisfiesM | — | — |
SatisfiesM_StateT_eq 📖 | mathematical | — | SatisfiesM | — | — |
---