2分木の特定の位置にノードを挿入する関数

[Seasawher]

自作。

variable {α : Type}

/-- 2分木 -/
inductive BinTree (α : Type) where
  | empty
  | node : α → BinTree α → BinTree α → BinTree α
  deriving Repr, Inhabited

namespace BinTree

/-- ノードの2分木の中での位置 -/
inductive Path where
  | root
  | left : Path → Path
  | right : Path → Path

/-- 2分木の特定の位置に、ノードを挿入する -/
def insert (tree : BinTree α) (path : Path) (new : α) : BinTree α :=
  match tree, path with
  | empty, .root => .node new empty empty
  | empty, _ => panic! "path not found"
  | node _ _ _, .root => panic! "root node already exists"
  | node a left right, .left path =>
    let newTree := insert left path new
    .node a newTree right
  | node a left right, .right path =>
    let newTree := insert right path new
    .node a left newTree

#eval insert .empty .root 3
  |>.insert (.root |> .left) 5
  |>.insert (.root |> .right) 2

end BinTree