addExprs

Mathlib.Tactic.Linarith.Verification

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

Lean4

/-- `addExprs L` creates an `Expr` representing the sum of the elements of `L`, associated left. -/
def addExprs : List Expr → MetaM Expr
  | [] =>
    return
      q(0) -- This may not be of the intended type; use with caution.

  | L@(h :: _) => do
    let ⟨_, α, _⟩ ← inferTypeQ' h
    let inst : Q(AddMonoid $α) ←
      synthInstanceQ
          q(AddMonoid $α)
            -- This is not type safe; we just assume all the `Expr`s in the tail have the same type:

    return addExprs' inst L

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

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

Разделы

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

Аффилиация

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