Ord

Mathlib.Tactic.Linarith.Preprocessing

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

Lean4

/-- Ordering on `Expr`. -/
@[deprecated "Use `Expr.lt` and `Expr.equal` or `Expr.eqv` directly. \
        If you need to order expressions, consider ordering them by order seen, with AtomM." (since := "2025-08-31")]
def Ord : Ord Expr :=
  ⟨fun a b => if Expr.lt a b then .lt else if a.equal b then .eq else .gt⟩

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

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

Разделы

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

Аффилиация

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