addOccurrence

Mathlib.Tactic.CC.Addition

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.CC.CCM.addOccurrence

Lean4

/-- Update the `child` so its parent becomes `parent`. -/
def addOccurrence (parent child : Expr) (symmTable : Bool) : CCM Unit := do
  let childRoot ← getRoot child
  modify fun ccs =>
      { ccs with
        parents :=
          ccs.parents.alter childRoot fun ps? =>
            let ps := ps?.getD ∅
            ps.insert { expr := parent, symmTable } }

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

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

Разделы

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

Аффилиация

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