LawfulMonadState

📁 Source: Batteries/Control/LawfulMonadState.lean

Statistics

Metric	Count
Definitions `LawfulMonadStateOf`	1
Theorems `getModify_bind_modify`, `getModify_eq`, `getModify_id`, `get_bind_const`, `get_bind_get`, `get_bind_get_bind`, `get_bind_map_set`, `get_bind_set`, `get_bind_set_bind`, `get_map_const`, `get_seqRight`, `instEStateM`, `instReaderTOfLawfulMonad`, `instStateCpsT`, `instStateRefT'OfLawfulMonad`, `instStateTOfLawfulMonad`, `modifyGetThe_eq`, `modifyGet_eq`, `modifyGet_eq'`, `modifyThe_eq`, `modify_bind_get`, `modify_bind_modify`, `modify_bind_modifyGet`, `modify_comm_of_comp_comm`, `modify_eq`, `modify_id`, `seqLeft_get`, `set_bind_get`, `set_bind_getModify`, `set_bind_getModify_bind`, `set_bind_get_bind`, `set_bind_map_get`, `set_bind_map_set`, `set_bind_modify`, `set_bind_modifyGet`, `set_bind_modifyGet_bind`, `set_bind_modify_bind`, `set_bind_set`, `set_bind_set_bind`, `toLawfulMonad`, `liftM_get`, `liftM_getModify`, `liftM_modify`, `liftM_modifyGet`, `liftM_set`, `monadStateOf_get_eq_get`, `monadStateOf_modifyGet_eq_modifyGet`	47
Total	48

LawfulMonadStateOf

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`getModify_bind_modify` 📖	—	—	—	—	`getModify_eq` `toLawfulMonad` `modify_eq` `set_bind_get_bind` `set_bind_set` `get_bind_get_bind`
`getModify_eq` 📖	—	—	—	—	`modifyGet_eq` `toLawfulMonad`
`getModify_id` 📖	—	—	—	—	`getModify_eq` `toLawfulMonad` `get_bind_map_set`
`get_bind_const` 📖	—	—	—	—	—
`get_bind_get` 📖	—	—	—	—	`get_bind_const`
`get_bind_get_bind` 📖	—	—	—	—	—
`get_bind_map_set` 📖	—	—	—	—	`toLawfulMonad` `get_bind_set_bind`
`get_bind_set` 📖	—	—	—	—	`toLawfulMonad` `get_map_const` `get_bind_set_bind`
`get_bind_set_bind` 📖	—	—	—	—	—
`get_map_const` 📖	—	—	—	—	`toLawfulMonad` `get_bind_const`
`get_seqRight` 📖	—	—	—	—	`toLawfulMonad` `get_bind_const`
`instEStateM` 📖	mathematical	—	`LawfulMonadStateOf`	—	—
`instReaderTOfLawfulMonad` 📖	mathematical	—	`LawfulMonadStateOf`	—	`modifyGet_eq` `get_bind_const` `get_bind_get_bind` `get_bind_set_bind` `set_bind_get` `set_bind_set`
`instStateCpsT` 📖	mathematical	—	`LawfulMonadStateOf`	—	—
`instStateRefT'OfLawfulMonad` 📖	mathematical	—	`LawfulMonadStateOf`	—	`instReaderTOfLawfulMonad`
`instStateTOfLawfulMonad` 📖	mathematical	—	`LawfulMonadStateOf`	—	—
`modifyGetThe_eq` 📖	—	—	—	—	`modifyGet_eq`
`modifyGet_eq` 📖	—	—	—	—	—
`modifyGet_eq'` 📖	—	—	—	—	`modifyGet_eq` `toLawfulMonad` `modify_eq` `get_bind_get_bind`
`modifyThe_eq` 📖	—	—	—	—	`modify_eq`
`modify_bind_get` 📖	—	—	—	—	`modify_eq` `toLawfulMonad` `set_bind_get` `get_bind_get_bind`
`modify_bind_modify` 📖	—	—	—	—	`modify_eq` `toLawfulMonad` `set_bind_get_bind` `set_bind_set`
`modify_bind_modifyGet` 📖	—	—	—	—	`modify_eq` `modifyGet_eq` `toLawfulMonad` `set_bind_get_bind` `set_bind_map_set`
`modify_comm_of_comp_comm` 📖	—	—	—	—	`modify_bind_modify`
`modify_eq` 📖	—	—	—	—	`modifyGet_eq` `toLawfulMonad`
`modify_id` 📖	—	—	—	—	`modify_eq` `get_bind_set`
`seqLeft_get` 📖	—	—	—	—	`toLawfulMonad` `get_bind_const`
`set_bind_get` 📖	—	—	—	—	—
`set_bind_getModify` 📖	—	—	—	—	`getModify_eq` `toLawfulMonad` `set_bind_get_bind` `set_bind_map_set`
`set_bind_getModify_bind` 📖	—	—	—	—	`getModify_eq` `toLawfulMonad` `set_bind_get` `set_bind_map_set`
`set_bind_get_bind` 📖	—	—	—	—	`toLawfulMonad` `set_bind_get`
`set_bind_map_get` 📖	—	—	—	—	`toLawfulMonad` `set_bind_get_bind`
`set_bind_map_set` 📖	—	—	—	—	`toLawfulMonad` `set_bind_set`
`set_bind_modify` 📖	—	—	—	—	`modify_eq` `set_bind_get_bind` `set_bind_set`
`set_bind_modifyGet` 📖	—	—	—	—	`modifyGet_eq` `toLawfulMonad` `set_bind_get_bind` `set_bind_map_set`
`set_bind_modifyGet_bind` 📖	—	—	—	—	`modifyGet_eq` `toLawfulMonad` `set_bind_get_bind` `set_bind_set_bind`
`set_bind_modify_bind` 📖	—	—	—	—	`modify_eq` `toLawfulMonad` `set_bind_get` `set_bind_set`
`set_bind_set` 📖	—	—	—	—	—
`set_bind_set_bind` 📖	—	—	—	—	`toLawfulMonad` `set_bind_set`
`toLawfulMonad` 📖	—	—	—	—	—

(root)

Definitions

Name	Category	Theorems
`LawfulMonadStateOf` 📖	CompData	6 math math: `OptionT.instLawfulMonadStateOfOfLawfulMonad`, `LawfulMonadStateOf.instReaderTOfLawfulMonad`, `LawfulMonadStateOf.instStateTOfLawfulMonad`, `LawfulMonadStateOf.instStateCpsT`, `LawfulMonadStateOf.instEStateM`, `LawfulMonadStateOf.instStateRefT'OfLawfulMonad`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`liftM_get` 📖	—	—	—	—	—
`liftM_getModify` 📖	—	—	—	—	—
`liftM_modify` 📖	—	—	—	—	—
`liftM_modifyGet` 📖	—	—	—	—	—
`liftM_set` 📖	—	—	—	—	—
`monadStateOf_get_eq_get` 📖	—	—	—	—	—
`monadStateOf_modifyGet_eq_modifyGet` 📖	—	—	—	—	—

---

← Back to Index