ExprMap

Mathlib.Tactic.Linarith.Parsing

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

Lean4

/-- `ExprMap` is used to record atomic expressions which have been seen while processing inequality
expressions.
-/
-- The natural number is just the index in the list,
-- and we could reimplement to just use `List Expr` if desired.

abbrev ExprMap :=
  List (Expr × ℕ)

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

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

Разделы

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

Аффилиация

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