Traversable

📁 Source: Mathlib/Data/Tree/Traversable.lean

Statistics

Metric	Count
Definitions instTraversable	1
Theorems comp_traverse, instLawfulTraversable, naturality, traverse_eq_map_id	4
Total	5

Tree

Definitions

Name	Category	Theorems
instTraversable 📖	CompOp	1 math math: instLawfulTraversable

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
comp_traverse 📖	mathematical	—	traverse Functor.Comp Functor.Comp.instApplicativeComp Tree	—	traverse.eq_1 traverse.eq_2 seq_map_assoc map_seq
instLawfulTraversable 📖	mathematical	—	LawfulTraversable Tree instTraversable	—	id_map comp_map traverse_pure CommApplicative.toLawfulApplicative instCommApplicativeId comp_traverse traverse_eq_map_id naturality
naturality 📖	mathematical	—	Tree traverse ApplicativeTransformation.app	—	traverse.eq_1 ApplicativeTransformation.preserves_pure traverse.eq_2 ApplicativeTransformation.preserves_seq ApplicativeTransformation.preserves_map
traverse_eq_map_id 📖	mathematical	—	traverse Tree map	—	traverse.eq_1 map.eq_1 traverse.eq_2 map.eq_2 CommApplicative.toLawfulApplicative instCommApplicativeId

---

← Back to Index