cmp — Mathlib

Lean4
/-- A comparator for propositions. (There should really be a derive handler for this.) -/
def cmp (p q : IProp) : Ordering := by
  cases p <;> cases q
  case var.var p q => exact compare p q
  case true.true => exact .eq
  case false.false => exact .eq
  case and'.and' ap p₁ p₂ aq q₁ q₂ => exact (ap.cmp aq).then <| (p₁.cmp q₁).then (p₂.cmp q₂)
  case or.or p₁ p₂ q₁ q₂ => exact (p₁.cmp q₁).then (p₂.cmp q₂)
  case imp.imp p₁ p₂ q₁ q₂ => exact (p₁.cmp q₁).then (p₂.cmp q₂)
  exacts [.lt, .lt, .lt, .lt, .lt, .gt, .lt, .lt, .lt, .lt, .gt, .gt, .lt, .lt, .lt, .gt, .gt, .gt, .lt, .lt, .gt, .gt,
    .gt, .gt, .lt, .gt, .gt, .gt, .gt, .gt]
Похожие утверждения