Monad

📁 Source: Mathlib/Data/List/Monad.lean

Statistics

Metric	Count
Definitions instAlternativeMonad_mathlib, instMonad	2
Theorems instLawfulAlternative_mathlib, instLawfulMonad, pure_def	3
Total	5

List

Definitions

Name	Category	Theorems
instAlternativeMonad_mathlib 📖	CompOp	5 math math: map_pure_sublist_sublists, instLawfulAlternative_mathlib, Turing.ToPartrec.Code.exists_code, flatMap_pure_eq_map, mem_pure
instMonad 📖	CompOp	5 math math: sublists_append, sublists_cons, bind_eq_flatMap, pure_def, instLawfulMonad

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instLawfulAlternative_mathlib 📖	mathematical	—	instAlternativeMonad_mathlib	—	instLawfulMonad
instLawfulMonad 📖	mathematical	—	instMonad	—	—
pure_def 📖	mathematical	—	instMonad	—	—

---

← Back to Index