checkNewSubsingletonEq — Mathlib

Lean4
/-- Given the equivalent expressions `oldRoot` and `newRoot` the root of `oldRoot` is
`newRoot`, if `oldRoot` has root representative of subsingletons, try to push the equality proof
between their root representatives to the todo list, or update the root representative to
`newRoot`. -/
def checkNewSubsingletonEq (oldRoot newRoot : Expr) : CCM Unit := do
  guard (← isEqv oldRoot newRoot)
  guard ((← getRoot oldRoot) == newRoot)
  let some it₁ := (← get).subsingletonReprs[oldRoot]? |
    return
  if let some it₂ := (← get).subsingletonReprs[newRoot]? then
    pushSubsingletonEq it₁ it₂
  else
    modify fun ccs => { ccs with subsingletonReprs := ccs.subsingletonReprs.insert newRoot it₁ }
Похожие утверждения