append

Mathlib.Lean.Meta.RefinedDiscrTree.Initialize

URI: https://scilib.ai/kg/mathlib#Lean.Meta.RefinedDiscrTree.PreDiscrTree.append

Lean4

/-- Merge two discrimination trees. -/
def append (x y : PreDiscrTree α) : PreDiscrTree α :=
  let (x, y, f) := if x.root.size ≥ y.root.size then (x, y, fun y x => x ++ y) else (y, x, fun x y => x ++ y)
  let { root := yk, tries := ya } := y
  yk.fold (init := x) fun d k yi => d.modifyAt k (f ya[yi]!)

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru