Documentation Verification Report

Cont

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

Statistics

Metric	Count
Definitions `Cont`, `ContT`, `equiv`, `instMonad`, `instMonadCont`, `instMonadExcept`, `instMonadLiftOfMonad`, `map`, `monadLift`, `run`, `withContT`, `callCC`, `mkLabel`, `LawfulMonadCont`, `MonadCont`, `Label`, `apply`, `callCC`, `goto`, `callCC`, `mkLabel`, `callCC`, `mkLabel`, `callCC`, `mkLabel`, `Cont`, `callCC`, `callCC'`, `mkLabel`, `mkLabel'`, `instMonadContExceptT`, `instMonadContOptionT`, `instMonadContReaderT`, `instMonadContStateT`, `instMonadContWriterTOfMonadOfEmptyCollection`, `instMonadContWriterTOfMonadOfMonoid`	36
Theorems `ext`, `ext_iff`, `instLawfulMonad`, `instLawfulMonadCont`, `monadLift_bind`, `run_contT_map_contT`, `run_withContT`, `goto_mkLabel`, `callCC_bind_left`, `callCC_bind_right`, `callCC_dummy`, `toLawfulMonad`, `goto_mkLabel`, `goto_mkLabel`, `goto_mkLabel`, `goto_mkLabel`, `goto_mkLabel'`, `instLawfulMonadContExceptT`, `instLawfulMonadContOptionT`, `instLawfulMonadContReaderT`, `instLawfulMonadContStateT`, `run_callCC`	22
Total	58

ContT

Definitions

Name	Category	Theorems
`equiv` 📖	CompOp	—
`instMonad` 📖	CompOp	3 math math: `instLawfulMonadCont`, `monadLift_bind`, `instLawfulMonad`
`instMonadCont` 📖	CompOp	1 math math: `instLawfulMonadCont`
`instMonadExcept` 📖	CompOp	—
`instMonadLiftOfMonad` 📖	CompOp	—
`map` 📖	CompOp	1 math math: `run_contT_map_contT`
`monadLift` 📖	CompOp	1 math math: `monadLift_bind`
`run` 📖	CompOp	3 math math: `run_withContT`, `ext_iff`, `run_contT_map_contT`
`withContT` 📖	CompOp	1 math math: `run_withContT`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`run`	—	—	—
`ext_iff` 📖	mathematical	—	`run`	—	`ext`
`instLawfulMonad` 📖	mathematical	—	`ContT` `instMonad`	—	`ext`
`instLawfulMonadCont` 📖	mathematical	—	`LawfulMonadCont` `ContT` `instMonad` `instMonadCont`	—	`instLawfulMonad` `ext`
`monadLift_bind` 📖	mathematical	—	`monadLift` `ContT` `instMonad`	—	`ext`
`run_contT_map_contT` 📖	mathematical	—	`run` `map`	—	—
`run_withContT` 📖	mathematical	—	`run` `withContT`	—	—

ExceptT

Definitions

Name	Category	Theorems
`callCC` 📖	CompOp	—
`mkLabel` 📖	CompOp	1 math math: `goto_mkLabel`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`goto_mkLabel` 📖	mathematical	—	`MonadCont.goto` `mkLabel`	—	—

LawfulMonadCont

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`callCC_bind_left` 📖	mathematical	—	`MonadCont.callCC` `MonadCont.goto`	—	—
`callCC_bind_right` 📖	mathematical	—	`MonadCont.callCC`	—	—
`callCC_dummy` 📖	mathematical	—	`MonadCont.callCC`	—	—
`toLawfulMonad` 📖	—	—	—	—	—

MonadCont

Definitions

Name	Category	Theorems
`Label` 📖	CompData	—
`callCC` 📖	CompOp	4 math math: `run_callCC`, `LawfulMonadCont.callCC_dummy`, `LawfulMonadCont.callCC_bind_left`, `LawfulMonadCont.callCC_bind_right`
`goto` 📖	CompOp	7 math math: `WriterT.goto_mkLabel`, `LawfulMonadCont.callCC_bind_left`, `ExceptT.goto_mkLabel`, `OptionT.goto_mkLabel`, `StateT.goto_mkLabel`, `WriterT.goto_mkLabel'`, `ReaderT.goto_mkLabel`

MonadCont.Label

Definitions

Name	Category	Theorems
`apply` 📖	CompOp	—

OptionT

Definitions

Name	Category	Theorems
`callCC` 📖	CompOp	1 math math: `run_callCC`
`mkLabel` 📖	CompOp	2 math math: `run_callCC`, `goto_mkLabel`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`goto_mkLabel` 📖	mathematical	—	`MonadCont.goto` `mkLabel`	—	—

ReaderT

Definitions

Name	Category	Theorems
`callCC` 📖	CompOp	—
`mkLabel` 📖	CompOp	1 math math: `goto_mkLabel`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`goto_mkLabel` 📖	mathematical	—	`MonadCont.goto` `mkLabel`	—	—

StateT

Definitions

Name	Category	Theorems
`callCC` 📖	CompOp	—
`mkLabel` 📖	CompOp	1 math math: `goto_mkLabel`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`goto_mkLabel` 📖	mathematical	—	`MonadCont.goto` `mkLabel`	—	—

Turing.ToPartrec

Definitions

Name	Category	Theorems
`Cont` 📖	CompData	—

WriterT

Definitions

Name	Category	Theorems
`callCC` 📖	CompOp	—
`callCC'` 📖	CompOp	—
`mkLabel` 📖	CompOp	1 math math: `goto_mkLabel`
`mkLabel'` 📖	CompOp	1 math math: `goto_mkLabel'`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`goto_mkLabel` 📖	mathematical	—	`MonadCont.goto` `WriterT` `mkLabel` `instMonadLiftOfEmptyCollection`	—	—
`goto_mkLabel'` 📖	mathematical	—	`MonadCont.goto` `WriterT` `mkLabel'` `instMonadLiftOfMonoid` `MulOne.toOne` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	—

(root)

Definitions

Name	Category	Theorems
`Cont` 📖	CompOp	—
`ContT` 📖	CompOp	3 math math: `ContT.instLawfulMonadCont`, `ContT.monadLift_bind`, `ContT.instLawfulMonad`
`LawfulMonadCont` 📖	CompData	5 math math: `ContT.instLawfulMonadCont`, `instLawfulMonadContStateT`, `instLawfulMonadContOptionT`, `instLawfulMonadContReaderT`, `instLawfulMonadContExceptT`
`MonadCont` 📖	CompData	—
`instMonadContExceptT` 📖	CompOp	1 math math: `instLawfulMonadContExceptT`
`instMonadContOptionT` 📖	CompOp	1 math math: `instLawfulMonadContOptionT`
`instMonadContReaderT` 📖	CompOp	1 math math: `instLawfulMonadContReaderT`
`instMonadContStateT` 📖	CompOp	1 math math: `instLawfulMonadContStateT`
`instMonadContWriterTOfMonadOfEmptyCollection` 📖	CompOp	—
`instMonadContWriterTOfMonadOfMonoid` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instLawfulMonadContExceptT` 📖	mathematical	—	`LawfulMonadCont` `instMonadContExceptT`	—	`LawfulMonadCont.toLawfulMonad` `LawfulMonadCont.callCC_bind_right` `LawfulMonadCont.callCC_dummy` `ExceptT.goto_mkLabel` `map_eq_bind_pure_comp` `LawfulMonadCont.callCC_bind_left`
`instLawfulMonadContOptionT` 📖	mathematical	—	`LawfulMonadCont` `instMonadContOptionT`	—	`LawfulMonadCont.toLawfulMonad` `run_callCC` `LawfulMonadCont.callCC_bind_right` `LawfulMonadCont.callCC_dummy` `OptionT.goto_mkLabel` `LawfulMonadCont.callCC_bind_left`
`instLawfulMonadContReaderT` 📖	mathematical	—	`LawfulMonadCont` `instMonadContReaderT`	—	`LawfulMonadCont.toLawfulMonad` `LawfulMonadCont.callCC_bind_right` `ReaderT.goto_mkLabel` `LawfulMonadCont.callCC_bind_left` `LawfulMonadCont.callCC_dummy`
`instLawfulMonadContStateT` 📖	mathematical	—	`LawfulMonadCont` `instMonadContStateT`	—	`LawfulMonadCont.toLawfulMonad` `LawfulMonadCont.callCC_bind_right` `StateT.goto_mkLabel` `LawfulMonadCont.callCC_bind_left` `LawfulMonadCont.callCC_dummy`
`run_callCC` 📖	mathematical	—	`OptionT.callCC` `MonadCont.callCC` `OptionT.mkLabel`	—	—

---

← Back to Index