instToStringAtomicFact

Mathlib.Tactic.Order.CollectFacts

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.Order.instToStringAtomicFact

Lean4

instance : ToString AtomicFact where
  toString
    fa :=
    match fa with
    | .eq lhs rhs _ => s! "#{lhs } = #{rhs}"
    | .ne lhs rhs _ => s! "#{lhs } ≠ #{rhs}"
    | .le lhs rhs _ => s! "#{lhs } ≤ #{rhs}"
    | .nle lhs rhs _ => s! "¬ #{lhs } ≤ #{rhs}"
    | .lt lhs rhs _ => s! "#{lhs } < #{rhs}"
    | .nlt lhs rhs _ => s! "¬ #{lhs } < #{rhs}"
    | .isTop idx => s! "#{idx} := ⊤"
    | .isBot idx => s! "#{idx} := ⊥"
    | .isInf lhs rhs res => s! "#{res } := #{lhs } ⊓ #{rhs}"
    | .isSup lhs rhs res => s! "#{res } := #{lhs } ⊔ #{rhs}"

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

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

Разделы

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

Аффилиация

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