validate

Mathlib.Tactic.Linarith.Oracle.FourierMotzkin

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

Lean4

/-- Throws an exception if a contradictory `PComp` is contained in the current state. -/
def validate : LinarithM Unit := do
  match (← getPCompSet).toList.find? (fun p : PComp => p.isContr) with
  | none =>
    return ()
  | some c =>
    throwThe _ c

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

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

Разделы

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

Аффилиация

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