Documentation Verification Report

Basic

📁 Source: Mathlib/Control/Traversable/Basic.lean

Statistics

Metric	Count
Definitions `ApplicativeTransformation`, `app`, `comp`, `idTransformation`, `instCoeFunForallForall`, `instInhabited`, `LawfulTraversable`, `traverse`, `toFunctor`, `traverse`, `instTraversableId`, `instTraversableList`, `instTraversableOption`, `instTraversableSum`, `sequence`	15
Theorems `app_eq_coe`, `coe_inj`, `coe_mk`, `comp_apply`, `comp_assoc`, `comp_id`, `congr_arg`, `congr_fun`, `ext`, `ext_iff`, `id_comp`, `preserves_map`, `preserves_map'`, `preserves_pure`, `preserves_pure'`, `preserves_seq`, `preserves_seq'`, `comp_traverse`, `id_traverse`, `naturality`, `toLawfulFunctor`, `traverse_eq_map_id`, `instLawfulTraversableId`	23
Total	38

ApplicativeTransformation

Definitions

Name	Category	Theorems
`app` 📖	CompOp	5 math math: `preserves_pure'`, `app_eq_coe`, `preserves_seq'`, `coe_mk`, `Tree.naturality`
`comp` 📖	CompOp	3 math math: `id_comp`, `comp_assoc`, `comp_id`
`idTransformation` 📖	CompOp	2 math math: `id_comp`, `comp_id`
`instCoeFunForallForall` 📖	CompOp	—
`instInhabited` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`app_eq_coe` 📖	mathematical	—	`app`	—	—
`coe_inj` 📖	—	`app`	—	—	—
`coe_mk` 📖	mathematical	—	`app`	—	—
`comp_apply` 📖	—	—	—	—	—
`comp_assoc` 📖	mathematical	—	`comp`	—	—
`comp_id` 📖	mathematical	—	`comp` `idTransformation`	—	`ext`
`congr_arg` 📖	—	—	—	—	—
`congr_fun` 📖	—	—	—	—	—
`ext` 📖	—	—	—	—	—
`ext_iff` 📖	—	—	—	—	`ext`
`id_comp` 📖	mathematical	—	`comp` `idTransformation`	—	`ext`
`preserves_map` 📖	—	—	—	—	`preserves_seq` `preserves_pure`
`preserves_map'` 📖	—	—	—	—	`preserves_map`
`preserves_pure` 📖	—	—	—	—	`preserves_pure'`
`preserves_pure'` 📖	mathematical	—	`app`	—	—
`preserves_seq` 📖	—	—	—	—	`preserves_seq'`
`preserves_seq'` 📖	mathematical	—	`app`	—	—

LawfulTraversable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_traverse` 📖	mathematical	—	`Traversable.traverse` `Functor.Comp` `Functor.Comp.instApplicativeComp`	—	—
`id_traverse` 📖	mathematical	—	`Traversable.traverse`	—	—
`naturality` 📖	mathematical	—	`Traversable.traverse`	—	—
`toLawfulFunctor` 📖	mathematical	—	`Traversable.toFunctor`	—	—
`traverse_eq_map_id` 📖	mathematical	—	`Traversable.traverse` `Traversable.toFunctor`	—	—

Sum

Definitions

Name	Category	Theorems
`traverse` 📖	CompOp	6 math math: `comp_traverse`, `naturality`, `traverse_eq_map_id`, `id_traverse`, `map_traverse`, `traverse_map`

Traversable

Definitions

Name	Category	Theorems
`toFunctor` 📖	CompOp	21 math math: `map_traverse'`, `Equiv.traverse_eq_map_id`, `foldl_map`, `LawfulTraversable.toLawfulFunctor`, `traverse_map'`, `comp_sequence`, `naturality'`, `map_eq_traverse_id`, `foldMap_map`, `traverse_map`, `LawfulTraversable.traverse_eq_map_id`, `foldlm_map`, `id_sequence`, `Sum.traverse_eq_map_id`, `foldr_map`, `traverse_eq_map_id'`, `toList_map`, `map_traverse`, `Sum.map_traverse`, `Sum.traverse_map`, `foldrm_map`
`traverse` 📖	CompOp	42 math math: `FreeSemigroup.traverse_pure'`, `List.traverse_cons`, `Filter.mem_traverse_iff`, `map_traverse'`, `LawfulTraversable.comp_traverse`, `FreeAddMagma.traverse_add`, `LawfulTraversable.id_traverse`, `FreeMagma.traverse_mul`, `Equiv.traverse_def`, `FreeAddMagma.traverse_eq`, `pure_traverse`, `FreeSemigroup.traverse_mul'`, `FreeSemigroup.traverse_mul`, `traverse_map'`, `FreeSemigroup.traverse_pure`, `traverse_id`, `Filter.mem_traverse`, `map_eq_traverse_id`, `FreeAddSemigroup.traverse_pure'`, `naturality_pf`, `FreeAddSemigroup.traverse_add`, `traverse_map`, `FreeAddSemigroup.traverse_add'`, `LawfulTraversable.naturality`, `FreeAddMagma.traverse_pure'`, `LawfulTraversable.traverse_eq_map_id`, `FreeAddMagma.traverse_add'`, `List.traverse_nil`, `traverse_eq_map_id'`, `FreeAddSemigroup.traverse_pure`, `FreeSemigroup.traverse_eq`, `FreeMagma.traverse_pure`, `map_traverse`, `nhds_list`, `FreeMagma.traverse_mul'`, `FreeMagma.traverse_eq`, `traverse_comp`, `List.mem_traverse`, `FreeAddMagma.traverse_pure`, `List.traverse_append`, `FreeMagma.traverse_pure'`, `FreeAddSemigroup.traverse_eq`

(root)

Definitions

Name	Category	Theorems
`ApplicativeTransformation` 📖	CompData	—
`LawfulTraversable` 📖	CompData	14 math math: `List.instLawfulTraversable`, `Equiv.isLawfulTraversable'`, `Bitraversable.isLawfulTraversable`, `FreeMagma.instLawfulTraversable`, `FreeSemigroup.instLawfulTraversable`, `Batteries.instLawfulTraversableDList`, `Sum.instLawfulTraversable`, `instLawfulTraversableOption`, `List.Vector.instLawfulTraversableFlipNat`, `Tree.instLawfulTraversable`, `FreeAddMagma.instLawfulTraversable`, `Equiv.isLawfulTraversable`, `instLawfulTraversableId`, `FreeAddSemigroup.instLawfulTraversable`
`instTraversableId` 📖	CompOp	1 math math: `instLawfulTraversableId`
`instTraversableList` 📖	CompOp	10 math math: `List.instLawfulTraversable`, `List.traverse_cons`, `Filter.mem_traverse_iff`, `Traversable.toList_eq_self`, `Filter.sequence_mono`, `Filter.mem_traverse`, `List.traverse_nil`, `nhds_list`, `List.mem_traverse`, `List.traverse_append`
`instTraversableOption` 📖	CompOp	1 math math: `instLawfulTraversableOption`
`instTraversableSum` 📖	CompOp	4 math math: `Sum.instLawfulTraversable`, `Sum.traverse_eq_map_id`, `Sum.map_traverse`, `Sum.traverse_map`
`sequence` 📖	CompOp	5 math math: `Filter.mem_traverse_iff`, `Filter.sequence_mono`, `Traversable.comp_sequence`, `Traversable.naturality'`, `Traversable.id_sequence`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instLawfulTraversableId` 📖	mathematical	—	`LawfulTraversable` `instTraversableId`	—	—

---

← Back to Index