push

Mathlib.Lean.Meta.RefinedDiscrTree.Initialize

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

Lean4

/-- Add an entry to the pre-discrimination tree. -/
def push (d : PreDiscrTree α) (k : Key) (e : LazyEntry × α) : PreDiscrTree α :=
  d.modifyAt k (·.push e)

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

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

Разделы

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

Аффилиация

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