add

Mathlib.Tactic.Linarith.Datatypes

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

Lean4

/-- Add two `Linexp`s together componentwise.
Preserves sorting and uniqueness of the first argument.
-/
partial def add : Linexp → Linexp → Linexp
  | [], a => a
  | a, [] => a
  | (a@(n1, z1) :: t1), (b@(n2, z2) :: t2) =>
    if n1 < n2 then b :: add (a :: t1) t2
    else
      if n2 < n1 then a :: add t1 (b :: t2)
      else
        let sum := z1 + z2
        if sum = 0 then add t1 t2 else (n1, sum) :: add t1 t2

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

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

Разделы

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

Аффилиация

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