insert

Mathlib.Tactic.Linarith.Frontend

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

Lean4

/-- Insert a new value into the map at key `k`. This does a defeq check with all other keys
in the map. -/
def insert {α : Type} (self : ExprMultiMap α) (k : Expr) (v : α) : MetaM (ExprMultiMap α) := do
  for h : i in [:self.size]do
    if ← isDefEq self[i].1 k then
      return self.modify i fun (k, vs) => (k, v :: vs)
  return self.push (k, [v])

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

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

Разделы

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

Аффилиация

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