Applicative 使用例： Tree の traverse

/-- A binary tree with values stored in non-leaf nodes. -/
inductive Tree.{u} (α : Type u) : Type u
  | nil : Tree α
  | node : α → Tree α → Tree α → Tree α
  deriving DecidableEq, Repr
compile_inductive% Tree

namespace Tree

universe u

variable {α : Type u}

instance : Inhabited (Tree α) :=
  ⟨nil⟩

/--
Do an action for every node of the tree.
Actions are taken in node -> left subtree -> right subtree recursive order.
This function is the `traverse` function for the `Traversable Tree` instance.
-/
def traverse {m : Type* → Type*} [Applicative m] {α β} (f : α → m β) : Tree α → m (Tree β)
  | .nil => pure nil
  | .node a l r => .node <$> f a <*> traverse f l <*> traverse f r

The issue provides a Lean definition of Tree and its traverse function, but names no target file or test. First locate the repository entry point for code examples or the mdBook documentation, then determine where this Applicative example belongs; done means the Tree traverse example is included in the appropriate documentation and renders or builds successfully.