Writer

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

Statistics

Metric	Count
Definitions MonadWriter, listen, pass, tell, MonadWriterAdapter, adaptWriter, Writer, WriterT, adapt, equiv, instMonadControlOfMonadLiftT, instMonadExcept, instMonadFunctor, instMonadLiftOfEmptyCollection, instMonadLiftOfMonoid, instMonadOfEmptyCollectionOfAppend, instMonadOfMonoid, instMonadWriter, liftTell, mk, monad, run, runThe, instMonadWriterAdapterWriterTOfMonad, instMonadWriterReaderT, instMonadWriterStateTOfMonad, monadWriterAdapterTrans	27
Theorems ext, ext_iff, instLawfulMonad	3
Total	30

MonadWriter

Definitions

Name	Category	Theorems
listen 📖	CompOp	—
pass 📖	CompOp	—
tell 📖	CompOp	—

MonadWriterAdapter

Definitions

Name	Category	Theorems
adaptWriter 📖	CompOp	—

WriterT

Definitions

Name	Category	Theorems
adapt 📖	CompOp	—
equiv 📖	CompOp	—
instMonadControlOfMonadLiftT 📖	CompOp	—
instMonadExcept 📖	CompOp	—
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	—
liftTell 📖	CompOp	—
mk 📖	CompOp	—
monad 📖	CompOp	—
run 📖	CompOp	1 math math: ext_iff
runThe 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ext 📖	—	run	—	—	—
ext_iff 📖	mathematical	—	run	—	ext
instLawfulMonad 📖	mathematical	—	WriterT instMonadOfMonoid	—	one_mul mul_assoc mul_one

(root)

Definitions

Name	Category	Theorems
MonadWriter 📖	CompData	—
MonadWriterAdapter 📖	CompData	—
Writer 📖	CompOp	—
WriterT 📖	CompOp	3 math math: WriterT.goto_mkLabel, WriterT.instLawfulMonad, WriterT.goto_mkLabel'
instMonadWriterAdapterWriterTOfMonad 📖	CompOp	—
instMonadWriterReaderT 📖	CompOp	—
instMonadWriterStateTOfMonad 📖	CompOp	—
monadWriterAdapterTrans 📖	CompOp	—

---

← Back to Index