toCompFold

Mathlib.Tactic.Linarith.Parsing

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Linarith.toCompFold

Lean4

/-- `toCompFold red e_map exprs monom_map` folds `toComp` over `exprs`,
updating `e_map` and `monom_map` as it goes.
-/
def toCompFold (red : TransparencyMode) : ExprMap → List Expr → Map Monom ℕ → MetaM (List Comp × ExprMap × Map Monom ℕ)
  | m, [], mm => return ([], m, mm)
  | m, (h :: t), mm => do
    let (c, m', mm') ← toComp red h m mm
    let (l, mp, mm') ← toCompFold red m' t mm'
    return (c :: l, mp, mm')

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

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

Разделы

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

Аффилиация

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