Documentation Verification Report

Effects

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

Statistics

Metric	Count
Definitions `ContF`, `FreeCont`, `callCC`, `contInterp`, `instMonadCont`, `run`, `toContT`, `FreeReader`, `instMonadReader`, `instMonadReaderOf`, `instMonadWithReaderOf`, `go`, `readInterp`, `run`, `toReaderM`, `FreeState`, `instMonadStateOf`, `run`, `run'`, `stateInterp`, `toStateM`, `FreeWriter`, `instMonadWriterOfMonoid`, `listen`, `pass`, `run`, `tell`, `toWriterT`, `writerInterp`, `ReaderF`, `StateF`, `WriterF`, `instFunctorContF`	33
Theorems `callCC_def`, `run_callCC`, `run_liftBind_callCC`, `run_pure`, `run_toContT`, `toContT_unique`, `read_def`, `run_pure`, `run_read`, `run_toReaderM`, `run_withReader`, `toReaderM_unique`, `get_def`, `run'_get`, `run'_pure`, `run'_set`, `run'_toStateM`, `run_get`, `run_pure`, `run_set`, `run_toStateM`, `set_def`, `toStateM_unique`, `listen_liftBind_tell`, `listen_pure`, `pass_def`, `run_liftBind_tell`, `run_pure`, `run_toWriterT`, `tell_def`, `toWriterT_unique`	31
Total	64

Cslib.FreeM

Definitions

Name	Category	Theorems
`ContF` 📖	CompData	4 math math: `FreeCont.callCC_def`, `FreeCont.run_pure`, `FreeCont.run_callCC`, `FreeCont.run_liftBind_callCC`
`FreeCont` 📖	CompOp	2 math math: `FreeCont.callCC_def`, `FreeCont.run_callCC`
`FreeReader` 📖	CompOp	2 math math: `FreeReader.read_def`, `FreeReader.run_withReader`
`FreeState` 📖	CompOp	2 math math: `FreeState.get_def`, `FreeState.set_def`
`FreeWriter` 📖	CompOp	—
`ReaderF` 📖	CompData	3 math math: `FreeReader.run_read`, `FreeReader.read_def`, `FreeReader.run_pure`
`StateF` 📖	CompData	8 math math: `FreeState.run'_set`, `FreeState.run_pure`, `FreeState.run_set`, `FreeState.run'_get`, `FreeState.run'_pure`, `FreeState.get_def`, `FreeState.set_def`, `FreeState.run_get`
`WriterF` 📖	CompData	5 math math: `FreeWriter.listen_liftBind_tell`, `FreeWriter.run_liftBind_tell`, `FreeWriter.run_pure`, `FreeWriter.listen_pure`, `FreeWriter.tell_def`
`instFunctorContF` 📖	CompOp	—

Cslib.FreeM.FreeCont

Definitions

Name	Category	Theorems
`callCC` 📖	CompOp	2 math math: `callCC_def`, `run_callCC`
`contInterp` 📖	CompOp	—
`instMonadCont` 📖	CompOp	—
`run` 📖	CompOp	5 math math: `callCC_def`, `run_pure`, `run_toContT`, `run_callCC`, `run_liftBind_callCC`
`toContT` 📖	CompOp	2 math math: `toContT_unique`, `run_toContT`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`callCC_def` 📖	mathematical	—	`callCC` `Cslib.FreeM.liftBind` `Cslib.FreeM.ContF` `Cslib.FreeM.ContF.callCC` `run` `Cslib.FreeM.FreeCont` `Cslib.FreeM` `Cslib.FreeM.instPure`	—	—
`run_callCC` 📖	mathematical	—	`run` `callCC` `Cslib.FreeM.FreeCont` `Cslib.FreeM.liftBind` `Cslib.FreeM.ContF` `Cslib.FreeM.ContF.callCC` `Cslib.FreeM` `Cslib.FreeM.instPure`	—	—
`run_liftBind_callCC` 📖	mathematical	—	`run` `Cslib.FreeM.liftBind` `Cslib.FreeM.ContF` `Cslib.FreeM.ContF.callCC`	—	—
`run_pure` 📖	mathematical	—	`run` `Cslib.FreeM.pure` `Cslib.FreeM.ContF`	—	—
`run_toContT` 📖	mathematical	—	`toContT` `run`	—	—
`toContT_unique` 📖	mathematical	`Cslib.FreeM.Interprets` `Cslib.FreeM.ContF` `contInterp`	`toContT`	—	`Cslib.FreeM.Interprets.eq`

Cslib.FreeM.FreeReader

Definitions

Name	Category	Theorems
`instMonadReader` 📖	CompOp	—
`instMonadReaderOf` 📖	CompOp	1 math math: `read_def`
`instMonadWithReaderOf` 📖	CompOp	1 math math: `run_withReader`
`readInterp` 📖	CompOp	—
`run` 📖	CompOp	4 math math: `run_read`, `run_withReader`, `run_pure`, `run_toReaderM`
`toReaderM` 📖	CompOp	2 math math: `toReaderM_unique`, `run_toReaderM`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`read_def` 📖	mathematical	—	`Cslib.FreeM.FreeReader` `instMonadReaderOf` `Cslib.FreeM.lift` `Cslib.FreeM.ReaderF` `Cslib.FreeM.ReaderF.read`	—	—
`run_pure` 📖	mathematical	—	`run` `Cslib.FreeM.pure` `Cslib.FreeM.ReaderF`	—	—
`run_read` 📖	mathematical	—	`run` `Cslib.FreeM.liftBind` `Cslib.FreeM.ReaderF` `Cslib.FreeM.ReaderF.read`	—	—
`run_toReaderM` 📖	mathematical	—	`toReaderM` `run`	—	—
`run_withReader` 📖	mathematical	—	`run` `Cslib.FreeM.FreeReader` `instMonadWithReaderOf`	—	—
`toReaderM_unique` 📖	mathematical	`Cslib.FreeM.Interprets` `Cslib.FreeM.ReaderF` `readInterp`	`toReaderM`	—	`Cslib.FreeM.Interprets.eq`

Cslib.FreeM.FreeReader.instMonadWithReaderOf

Definitions

Name	Category	Theorems
`go` 📖	CompOp	—

Cslib.FreeM.FreeState

Definitions

Name	Category	Theorems
`instMonadStateOf` 📖	CompOp	2 math math: `get_def`, `set_def`
`run` 📖	CompOp	4 math math: `run_pure`, `run_set`, `run_toStateM`, `run_get`
`run'` 📖	CompOp	4 math math: `run'_set`, `run'_get`, `run'_pure`, `run'_toStateM`
`stateInterp` 📖	CompOp	—
`toStateM` 📖	CompOp	3 math math: `run_toStateM`, `run'_toStateM`, `toStateM_unique`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`get_def` 📖	mathematical	—	`Cslib.FreeM.FreeState` `instMonadStateOf` `Cslib.FreeM.lift` `Cslib.FreeM.StateF` `Cslib.FreeM.StateF.get`	—	—
`run'_get` 📖	mathematical	—	`run'` `Cslib.FreeM.liftBind` `Cslib.FreeM.StateF` `Cslib.FreeM.StateF.get`	—	—
`run'_pure` 📖	mathematical	—	`run'` `Cslib.FreeM.pure` `Cslib.FreeM.StateF`	—	—
`run'_set` 📖	mathematical	—	`run'` `Cslib.FreeM.liftBind` `Cslib.FreeM.StateF` `Cslib.FreeM.StateF.set`	—	—
`run'_toStateM` 📖	mathematical	—	`toStateM` `run'`	—	`run'.eq_1` `run_toStateM`
`run_get` 📖	mathematical	—	`run` `Cslib.FreeM.liftBind` `Cslib.FreeM.StateF` `Cslib.FreeM.StateF.get`	—	—
`run_pure` 📖	mathematical	—	`run` `Cslib.FreeM.pure` `Cslib.FreeM.StateF`	—	—
`run_set` 📖	mathematical	—	`run` `Cslib.FreeM.liftBind` `Cslib.FreeM.StateF` `Cslib.FreeM.StateF.set`	—	—
`run_toStateM` 📖	mathematical	—	`toStateM` `run`	—	—
`set_def` 📖	mathematical	—	`Cslib.FreeM.FreeState` `instMonadStateOf` `Cslib.FreeM.lift` `Cslib.FreeM.StateF` `Cslib.FreeM.StateF.set`	—	—
`toStateM_unique` 📖	mathematical	`Cslib.FreeM.Interprets` `Cslib.FreeM.StateF` `stateInterp`	`toStateM`	—	`Cslib.FreeM.Interprets.eq`

Cslib.FreeM.FreeWriter

Definitions

Name	Category	Theorems
`instMonadWriterOfMonoid` 📖	CompOp	—
`listen` 📖	CompOp	2 math math: `listen_liftBind_tell`, `listen_pure`
`pass` 📖	CompOp	1 math math: `pass_def`
`run` 📖	CompOp	3 math math: `run_toWriterT`, `run_liftBind_tell`, `run_pure`
`tell` 📖	CompOp	1 math math: `tell_def`
`toWriterT` 📖	CompOp	2 math math: `run_toWriterT`, `toWriterT_unique`
`writerInterp` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`listen_liftBind_tell` 📖	mathematical	—	`listen` `Cslib.FreeM.liftBind` `Cslib.FreeM.WriterF` `Cslib.FreeM.WriterF.tell` `Cslib.FreeM` `Cslib.FreeM.instBind` `Cslib.FreeM.instPure`	—	—
`listen_pure` 📖	mathematical	—	`listen` `Cslib.FreeM.pure` `Cslib.FreeM.WriterF`	—	—
`pass_def` 📖	mathematical	—	`pass`	—	—
`run_liftBind_tell` 📖	mathematical	—	`run` `Cslib.FreeM.liftBind` `Cslib.FreeM.WriterF` `Cslib.FreeM.WriterF.tell`	—	—
`run_pure` 📖	mathematical	—	`run` `Cslib.FreeM.pure` `Cslib.FreeM.WriterF`	—	—
`run_toWriterT` 📖	mathematical	—	`toWriterT` `run`	—	`Cslib.FreeM.liftM_liftBind`
`tell_def` 📖	mathematical	—	`tell` `Cslib.FreeM.lift` `Cslib.FreeM.WriterF` `Cslib.FreeM.WriterF.tell`	—	—
`toWriterT_unique` 📖	mathematical	`Cslib.FreeM.Interprets` `Cslib.FreeM.WriterF` `writerInterp`	`toWriterT`	—	`Cslib.FreeM.Interprets.eq`

---

← Back to Index