format

Mathlib.Tactic.ITauto

URI: https://scilib.ai/kg/mathlib#Mathlib.Tactic.ITauto.IProp.format

Lean4

/-- Debugging printer for propositions. -/
def format : IProp → Std.Format
  | .var i => f! "v{i}"
  | .true => f!"⊤"
  | .false => f!"⊥"
  | .and p q => f! "({p.format } ∧ {q.format})"
  | .iff p q => f! "({p.format } ↔ {q.format})"
  | .eq p q => f! "({p.format } = {q.format})"
  | .or p q => f! "({p.format } ∨ {q.format})"
  | .imp p q => f! "({p.format } → {q.format})"

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

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

Разделы

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

Аффилиация

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