getRoots

Mathlib.Tactic.CC.Datatypes

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.CC.CCState.getRoots

Lean4

/-- Append to `roots` all the roots of equivalence classes in `ccs`.

If `nonsingletonOnly` is true, we skip all the singleton equivalence classes. -/
def getRoots (ccs : CCState) (roots : Array Expr) (nonsingletonOnly : Bool) : Array Expr :=
  Id.run
    (do
      let mut roots := roots
      for (k, n) in ccs.entries do
        if k == n.root && (!nonsingletonOnly || !ccs.inSingletonEqc k) then
          roots := roots.push k
      return roots)

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

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

Разделы

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

Аффилиация

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