Theorems · Theorem · combinatorics

BinaryTree.traverse.eq_def

∀ {m : Type u_1 → Type u_2} [inst : Applicative m] {α : Type u_3} {β : Type u_1} (f : α → m β) (x : BinaryTree α),
  BinaryTree.traverse f x =
    match x with
    | BinaryTree.nil => pure BinaryTree.nil
    | BinaryTree.node a l r => BinaryTree.node <$> f a <*> BinaryTree.traverse f l <*> BinaryTree.traverse f r

Defined in

Mathlib.Data.Tree.Basic

Cited by

0 results in Mathlib

Foundations

Depth 7 from the axioms · uses no axioms

Assumes

Applicative