Documentation Verification Report

Instances

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

Statistics

Metric	Count
Definitions	0
Theorems `comp_traverse`, `id_traverse`, `instLawfulTraversable`, `mem_traverse`, `naturality`, `traverse_append`, `traverse_cons`, `traverse_eq_map_id`, `traverse_nil`, `comp_traverse`, `id_traverse`, `naturality`, `traverse_eq_map_id`, `comp_traverse`, `id_traverse`, `instLawfulTraversable`, `map_traverse`, `naturality`, `traverse_eq_map_id`, `traverse_map`, `instLawfulTraversableOption`	21
Total	21

List

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_traverse` 📖	mathematical	—	`Functor.Comp` `Functor.Comp.instApplicativeComp`	—	`seq_map_assoc` `map_seq`
`id_traverse` 📖	—	—	—	—	`CommApplicative.toLawfulApplicative` `instCommApplicativeId`
`instLawfulTraversable` 📖	mathematical	—	`LawfulTraversable` `instTraversableList`	—	`instLawfulMonad` `id_traverse` `comp_traverse` `traverse_eq_map_id` `naturality`
`mem_traverse` 📖	mathematical	—	`Set` `Set.instMembership` `Traversable.traverse` `instTraversableList` `Set.instAlternative`	—	—
`naturality` 📖	—	—	—	—	`ApplicativeTransformation.preserves_pure` `ApplicativeTransformation.preserves_seq` `ApplicativeTransformation.preserves_map`
`traverse_append` 📖	mathematical	—	`Traversable.traverse` `instTraversableList`	—	`pure_id'_seq` `seq_map_assoc` `map_seq`
`traverse_cons` 📖	mathematical	—	`Traversable.traverse` `instTraversableList`	—	—
`traverse_eq_map_id` 📖	—	—	—	—	`CommApplicative.toLawfulApplicative` `instCommApplicativeId`
`traverse_nil` 📖	mathematical	—	`Traversable.traverse` `instTraversableList`	—	—

Option

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_traverse` 📖	mathematical	—	`traverse` `Functor.Comp` `Functor.Comp.instApplicativeComp`	—	—
`id_traverse` 📖	mathematical	—	`traverse`	—	—
`naturality` 📖	mathematical	—	`traverse`	—	`ApplicativeTransformation.preserves_pure` `ApplicativeTransformation.preserves_map`
`traverse_eq_map_id` 📖	mathematical	—	`traverse`	—	—

Sum

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comp_traverse` 📖	mathematical	—	`traverse` `Functor.Comp` `Functor.Comp.instApplicativeComp`	—	—
`id_traverse` 📖	mathematical	—	`traverse`	—	—
`instLawfulTraversable` 📖	mathematical	—	`LawfulTraversable` `instTraversableSum`	—	`instLawfulMonad_mathlib` `id_traverse` `comp_traverse` `traverse_eq_map_id` `naturality`
`map_traverse` 📖	mathematical	—	`Traversable.toFunctor` `instTraversableSum` `traverse`	—	—
`naturality` 📖	mathematical	—	`traverse`	—	`ApplicativeTransformation.preserves_pure` `ApplicativeTransformation.preserves_map`
`traverse_eq_map_id` 📖	mathematical	—	`traverse` `Traversable.toFunctor` `instTraversableSum`	—	`CommApplicative.toLawfulApplicative` `instCommApplicativeId`
`traverse_map` 📖	mathematical	—	`traverse` `Traversable.toFunctor` `instTraversableSum`	—	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instLawfulTraversableOption` 📖	mathematical	—	`LawfulTraversable` `instTraversableOption`	—	`Option.id_traverse` `Option.comp_traverse` `Option.traverse_eq_map_id` `Option.naturality`

---

← Back to Index