Documentation Verification Report

Free

📁 Source: Cslib/Foundations/Control/Monad/Free.lean

Statistics

Metric	Count
Definitions `FreeM`, `Interprets`, `bind`, `instBind`, `instFunctor`, `instMonad`, `instPure`, `lift`, `liftM`, `map`	10
Theorems `apply_liftBind`, `apply_pure`, `eq`, `iff`, `liftM`, `bind_assoc`, `bind_eq_bind`, `bind_pure`, `bind_pure_comp`, `comp_map`, `id_map`, `instLawfulFunctor`, `instLawfulMonad`, `liftBind_bind`, `liftM_bind`, `liftM_lift`, `liftM_liftBind`, `liftM_pure`, `lift_def`, `map_eq_map`, `map_lift`, `pure_bind`, `pure_eq_pure`	23
Total	33

Cslib

Definitions

Name	Category	Theorems
`FreeM` 📖	CompData	9 math math: `FreeM.FreeWriter.listen_liftBind_tell`, `FreeM.instLawfulFunctor`, `FreeM.FreeCont.callCC_def`, `FreeM.bind_pure_comp`, `FreeM.bind_eq_bind`, `FreeM.pure_eq_pure`, `FreeM.FreeCont.run_callCC`, `FreeM.instLawfulMonad`, `FreeM.map_eq_map`

Cslib.FreeM

Definitions

Name	Category	Theorems
`Interprets` 📖	CompData	2 math math: `Interprets.liftM`, `Interprets.iff`
`bind` 📖	CompOp	7 math math: `pure_bind`, `liftM_bind`, `bind_pure_comp`, `bind_eq_bind`, `bind_assoc`, `liftBind_bind`, `bind_pure`
`instBind` 📖	CompOp	2 math math: `FreeWriter.listen_liftBind_tell`, `bind_eq_bind`
`instFunctor` 📖	CompOp	2 math math: `instLawfulFunctor`, `map_eq_map`
`instMonad` 📖	CompOp	1 math math: `instLawfulMonad`
`instPure` 📖	CompOp	4 math math: `FreeWriter.listen_liftBind_tell`, `FreeCont.callCC_def`, `pure_eq_pure`, `FreeCont.run_callCC`
`lift` 📖	CompOp	7 math math: `FreeState.get_def`, `map_lift`, `lift_def`, `FreeReader.read_def`, `liftM_lift`, `FreeState.set_def`, `FreeWriter.tell_def`
`liftM` 📖	CompOp	7 math math: `Interprets.liftM`, `Interprets.iff`, `liftM_bind`, `liftM_liftBind`, `Interprets.eq`, `liftM_lift`, `liftM_pure`
`map` 📖	CompOp	5 math math: `bind_pure_comp`, `id_map`, `map_lift`, `comp_map`, `map_eq_map`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bind_assoc` 📖	mathematical	—	`bind`	—	—
`bind_eq_bind` 📖	mathematical	—	`Cslib.FreeM` `instBind` `bind`	—	—
`bind_pure` 📖	mathematical	—	`bind` `pure`	—	—
`bind_pure_comp` 📖	mathematical	—	`bind` `Cslib.FreeM` `pure` `map`	—	—
`comp_map` 📖	mathematical	—	`map`	—	—
`id_map` 📖	mathematical	—	`map`	—	—
`instLawfulFunctor` 📖	mathematical	—	`Cslib.FreeM` `instFunctor`	—	`id_map` `comp_map`
`instLawfulMonad` 📖	mathematical	—	`Cslib.FreeM` `instMonad`	—	`id_map` `pure_bind` `bind_assoc` `bind_pure_comp`
`liftBind_bind` 📖	mathematical	—	`bind` `liftBind`	—	—
`liftM_bind` 📖	mathematical	—	`liftM` `bind`	—	`bind.eq_2` `liftM_liftBind`
`liftM_lift` 📖	mathematical	—	`liftM` `lift`	—	`liftM_liftBind`
`liftM_liftBind` 📖	mathematical	—	`liftM` `liftBind`	—	—
`liftM_pure` 📖	mathematical	—	`liftM` `pure`	—	—
`lift_def` 📖	mathematical	—	`lift` `liftBind` `pure`	—	—
`map_eq_map` 📖	mathematical	—	`Cslib.FreeM` `instFunctor` `map`	—	—
`map_lift` 📖	mathematical	—	`map` `lift` `liftBind` `pure`	—	—
`pure_bind` 📖	mathematical	—	`bind` `pure`	—	—
`pure_eq_pure` 📖	mathematical	—	`Cslib.FreeM` `instPure` `pure`	—	—

Cslib.FreeM.Interprets

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_liftBind` 📖	mathematical	`Cslib.FreeM.Interprets`	`Cslib.FreeM.liftBind`	—	—
`apply_pure` 📖	mathematical	`Cslib.FreeM.Interprets`	`Cslib.FreeM.pure`	—	—
`eq` 📖	mathematical	`Cslib.FreeM.Interprets`	`Cslib.FreeM.liftM`	—	`apply_pure` `Cslib.FreeM.liftM_liftBind` `apply_liftBind`
`iff` 📖	mathematical	—	`Cslib.FreeM.Interprets` `Cslib.FreeM.liftM`	—	`eq` `liftM`
`liftM` 📖	mathematical	—	`Cslib.FreeM.Interprets` `Cslib.FreeM.liftM`	—	—

---

← Back to Index