Traversable Binary Tree

Provides a Traversable instance for the Tree type.

instance Tree.instTraversable : Traversable Tree

Equations

• Tree.instTraversable = Traversable.mk fun {m : Type ?u.15 → Type ?u.15} [Applicative m] {α β : Type ?u.15} => Tree.traverse

theorem Tree.comp_traverse {α : Type u_1} {F : Type u → Type v} {G : Type v → Type w} [Applicative F] [Applicative G] [LawfulApplicative G] {β : Type v} {γ : Type u} (f : β → F γ) (g : α → G β) (t : Tree α) : traverse (Functor.Comp.mk ∘ (fun (x : G β) => f <$> x) ∘ g) t = Functor.Comp.mk ((fun (x : Tree β) => traverse f x) <$> traverse g t)

theorem Tree.traverse_eq_map_id {α : Type u_1} {β : Type u_2} (f : α → β) (t : Tree α) : traverse (pure ∘ f) t = map f t

theorem Tree.naturality {α : Type u_1} {F : Type u → Type u_3} {G : Type u → Type u_4} [Applicative F] [Applicative G] [LawfulApplicative F] [LawfulApplicative G] (η : ApplicativeTransformation F G) {β : Type u} (f : α → F β) (t : Tree α) : (fun {α : Type u} => η.app α) (traverse f t) = traverse (η.app β ∘ f) t

instance Tree.instLawfulTraversable : LawfulTraversable Tree