Documentation Verification Report

Erased

📁 Source: Mathlib/Data/Erased.lean

Statistics

Metric	Count
Definitions `Erased`, `OutType`, `bind`, `choice`, `equiv`, `instInhabitedOfNonempty`, `instRepr`, `instToString`, `join`, `map`, `mk`, `out`	12
Theorems `bind_def`, `bind_eq_out`, `instLawfulMonad`, `join_eq_out`, `map_def`, `map_out`, `mk_out`, `nonempty_iff`, `out_inj`, `out_inj_iff`, `out_mk`, `out_proof`, `pure_def`	13
Total	25

Erased

Definitions

Name	Category	Theorems
`OutType` 📖	CompOp	—
`bind` 📖	CompOp	2 math math: `bind_def`, `bind_eq_out`
`choice` 📖	CompOp	—
`equiv` 📖	CompOp	—
`instInhabitedOfNonempty` 📖	CompOp	—
`instRepr` 📖	CompOp	—
`instToString` 📖	CompOp	—
`join` 📖	CompOp	1 math math: `join_eq_out`
`map` 📖	CompOp	2 math math: `map_out`, `map_def`
`mk` 📖	CompOp	—
`out` 📖	CompOp	6 math math: `map_out`, `mk_out`, `out_inj_iff`, `bind_eq_out`, `out_mk`, `join_eq_out`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bind_def` 📖	mathematical	—	`Erased` `Monad` `bind`	—	—
`bind_eq_out` 📖	mathematical	—	`bind` `out`	—	—
`instLawfulMonad` 📖	mathematical	—	`Erased` `Monad`	—	`map_out` `mk_out`
`join_eq_out` 📖	mathematical	—	`join` `out` `Erased`	—	—
`map_def` 📖	mathematical	—	`Erased` `Monad` `map`	—	—
`map_out` 📖	mathematical	—	`out` `map`	—	—
`mk_out` 📖	mathematical	—	`out`	—	—
`nonempty_iff` 📖	mathematical	—	`Erased`	—	—
`out_inj` 📖	—	`out`	—	—	`mk_out`
`out_inj_iff` 📖	mathematical	—	`out`	—	—
`out_mk` 📖	mathematical	—	`out`	—	—
`out_proof` 📖	—	—	—	—	—
`pure_def` 📖	mathematical	—	`Erased` `Monad`	—	—

(root)

Definitions

Name	Category	Theorems
`Erased` 📖	CompOp	6 math math: `Erased.bind_def`, `Erased.pure_def`, `Erased.instLawfulMonad`, `Erased.join_eq_out`, `Erased.nonempty_iff`, `Erased.map_def`

---

← Back to Index