Documentation Verification Report

Writer

📁 Source: Mathlib/Control/Monad/Writer.lean

Statistics

Metric	Count
Definitions `MonadWriter`, `listen`, `pass`, `tell`, `MonadWriterAdapter`, `adaptWriter`, `Writer`, `WriterT`, `adapt`, `equiv`, `instMonadControlOfMonadLiftT`, `instMonadExceptOf`, `instMonadFunctor`, `instMonadLiftOfEmptyCollection`, `instMonadLiftOfMonoid`, `instMonadOfEmptyCollectionOfAppend`, `instMonadOfMonoid`, `instMonadWriter`, `liftTell`, `mk`, `monad`, `run`, `runThe`, `instMonadWriterAdapterWriterTOfMonad`, `instMonadWriterReaderT`, `instMonadWriterStateTOfMonad`, `monadWriterAdapterTrans`	27
Theorems `ext`, `ext_iff`, `instLawfulMonad`, `run_bind`, `run_liftM`, `run_listen`, `run_map`, `run_mk`, `run_pass`, `run_pure`, `run_tell`, `run_throw`, `run_tryCatch`	13
Total	40

MonadWriter

Definitions

Name	Category	Theorems
`listen` 📖	CompOp	1 math math: `WriterT.run_listen`
`pass` 📖	CompOp	1 math math: `WriterT.run_pass`
`tell` 📖	CompOp	1 math math: `WriterT.run_tell`

MonadWriterAdapter

Definitions

Name	Category	Theorems
`adaptWriter` 📖	CompOp	—

WriterT

Definitions

Name	Category	Theorems
`adapt` 📖	CompOp	—
`equiv` 📖	CompOp	—
`instMonadControlOfMonadLiftT` 📖	CompOp	—
`instMonadExceptOf` 📖	CompOp	2 math math: `run_throw`, `run_tryCatch`
`instMonadFunctor` 📖	CompOp	—
`instMonadLiftOfEmptyCollection` 📖	CompOp	1 math math: `goto_mkLabel`
`instMonadLiftOfMonoid` 📖	CompOp	1 math math: `goto_mkLabel'`
`instMonadOfEmptyCollectionOfAppend` 📖	CompOp	—
`instMonadOfMonoid` 📖	CompOp	1 math math: `instLawfulMonad`
`instMonadWriter` 📖	CompOp	3 math math: `run_tell`, `run_pass`, `run_listen`
`liftTell` 📖	CompOp	1 math math: `run_liftM`
`mk` 📖	CompOp	—
`monad` 📖	CompOp	3 math math: `run_map`, `run_bind`, `run_pure`
`run` 📖	CompOp	11 math math: `run_map`, `run_bind`, `run_throw`, `run_pure`, `run_tell`, `ext_iff`, `run_pass`, `run_listen`, `run_tryCatch`, `run_liftM`, `run_mk`
`runThe` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`run`	—	—	—
`ext_iff` 📖	mathematical	—	`run`	—	`ext`
`instLawfulMonad` 📖	mathematical	—	`WriterT` `instMonadOfMonoid`	—	`ext` `one_mul` `mul_assoc` `mul_one`
`run_bind` 📖	mathematical	—	`run` `WriterT` `monad`	—	—
`run_liftM` 📖	mathematical	—	`run` `WriterT` `liftTell`	—	—
`run_listen` 📖	mathematical	—	`run` `MonadWriter.listen` `WriterT` `instMonadWriter`	—	—
`run_map` 📖	mathematical	—	`run` `WriterT` `monad`	—	—
`run_mk` 📖	mathematical	—	`run`	—	—
`run_pass` 📖	mathematical	—	`run` `MonadWriter.pass` `WriterT` `instMonadWriter`	—	—
`run_pure` 📖	mathematical	—	`run` `WriterT` `monad`	—	—
`run_tell` 📖	mathematical	—	`run` `MonadWriter.tell` `WriterT` `instMonadWriter`	—	—
`run_throw` 📖	mathematical	—	`run` `WriterT` `instMonadExceptOf`	—	—
`run_tryCatch` 📖	mathematical	—	`run` `WriterT` `instMonadExceptOf`	—	—

(root)

Definitions

Name	Category	Theorems
`MonadWriter` 📖	CompData	—
`MonadWriterAdapter` 📖	CompData	—
`Writer` 📖	CompOp	—
`WriterT` 📖	CompOp	12 math math: `WriterT.run_map`, `WriterT.run_bind`, `WriterT.goto_mkLabel`, `WriterT.run_throw`, `WriterT.run_pure`, `WriterT.run_tell`, `WriterT.run_pass`, `WriterT.run_listen`, `WriterT.run_tryCatch`, `WriterT.instLawfulMonad`, `WriterT.goto_mkLabel'`, `WriterT.run_liftM`
`instMonadWriterAdapterWriterTOfMonad` 📖	CompOp	—
`instMonadWriterReaderT` 📖	CompOp	—
`instMonadWriterStateTOfMonad` 📖	CompOp	—
`monadWriterAdapterTrans` 📖	CompOp	—

---

← Back to Index