Basic

📁 Source: Mathlib/Control/Basic.lean

Statistics

Metric	Count
Definitions CommApplicative, mapAccumLM, mapAccumRM, bind, instMonad_mathlib, succeeds, try?, tryM, zipWithM, zipWithM'	10
Theorems commutative_map, commutative_prod, toLawfulApplicative, instLawfulFunctor_mathlib, instLawfulMonad_mathlib, fish_assoc, fish_pipe, fish_pure, guard_false, guard_true, joinM_map_joinM, joinM_map_map, joinM_map_pure, joinM_pure, map_seq, pure_id'_seq, seq_bind_eq, seq_map_assoc	18
Total	28

CommApplicative

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
commutative_map 📖	—	—	—	—	map_seq toLawfulApplicative commutative_prod
commutative_prod 📖	—	—	—	—	—
toLawfulApplicative 📖	—	—	—	—	—

List

Definitions

Name	Category	Theorems
mapAccumLM 📖	CompOp	—
mapAccumRM 📖	CompOp	—

Sum

Definitions

Name	Category	Theorems
bind 📖	CompOp	—
instMonad_mathlib 📖	CompOp	3 math math: instLawfulFunctor_mathlib, instLawfulMonad_mathlib, ManyOneDegree.add_of

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instLawfulFunctor_mathlib 📖	mathematical	—	instMonad_mathlib	—	—
instLawfulMonad_mathlib 📖	mathematical	—	instMonad_mathlib	—	instLawfulFunctor_mathlib

(root)

Definitions

Name	Category	Theorems
CommApplicative 📖	CompData	6 math math: Set.instCommApplicative, Filter.instCommApplicative, FreeAbelianGroup.instCommApplicative, Functor.Comp.instCommApplicative, Finset.commApplicative, instCommApplicativeId
succeeds 📖	CompOp	—
try? 📖	CompOp	—
tryM 📖	CompOp	—
zipWithM 📖	CompOp	—
zipWithM' 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
fish_assoc 📖	—	—	—	—	—
fish_pipe 📖	—	—	—	—	—
fish_pure 📖	—	—	—	—	—
guard_false 📖	—	—	—	—	—
guard_true 📖	—	—	—	—	—
joinM_map_joinM 📖	mathematical	—	joinM	—	—
joinM_map_map 📖	mathematical	—	joinM	—	—
joinM_map_pure 📖	mathematical	—	joinM	—	—
joinM_pure 📖	mathematical	—	joinM	—	—
map_seq 📖	—	—	—	—	—
pure_id'_seq 📖	—	—	—	—	—
seq_bind_eq 📖	—	—	—	—	—
seq_map_assoc 📖	—	—	—	—	—

---

← Back to Index