Traversable Binary Tree

Provides a Traversable instance for the Tree type.

@[implicit_reducible]

instance BinaryTree.instTraversable : Traversable BinaryTree

Equations

• BinaryTree.instTraversable = { map := fun {α β : Type ?u.1} => BinaryTree.map, traverse := fun {m : Type ?u.1 → Type ?u.1} [Applicative m] {α β : Type ?u.1} => BinaryTree.traverse }

theorem BinaryTree.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 : BinaryTree α) : traverse (Functor.Comp.mk ∘ (fun (x : G β) => f <$> x) ∘ g) t = Functor.Comp.mk ((fun (x : BinaryTree β) => traverse f x) <$> traverse g t)

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

theorem BinaryTree.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 : BinaryTree α) : (fun {α : Type u} => η.app α) (traverse f t) = traverse (η.app β ∘ f) t

instance BinaryTree.instLawfulTraversable : LawfulTraversable BinaryTree