inductive LO.Meta.Litform (α : Type u_1) : Type u_1

• atom {α : Type u_1} (a : α) : Litform α
• verum {α : Type u_1} : Litform α
• falsum {α : Type u_1} : Litform α
• and {α : Type u_1} : Litform α → Litform α → Litform α
• or {α : Type u_1} : Litform α → Litform α → Litform α
• neg {α : Type u_1} : Litform α → Litform α
• imply {α : Type u_1} : Litform α → Litform α → Litform α
• iff {α : Type u_1} : Litform α → Litform α → Litform α

@[implicit_reducible]

instance LO.Meta.Litform.instLogicalConnective {α : Type u_1} : LogicalConnective (Litform α)

Equations

• One or more equations did not get rendered due to their size.

def LO.Meta.Litform.toStr {α : Type u_1} [ToString α] : Litform α → String

Equations

• LO.Meta.Litform.verum.toStr = "⊤"
• LO.Meta.Litform.falsum.toStr = "⊥"
• (LO.Meta.Litform.atom a).toStr = toString "atom " ++ toString (toString a)
• φ.neg.toStr = "(¬" ++ φ.toStr ++ ")"
• (φ.and ψ).toStr = "(" ++ φ.toStr ++ " ∧ " ++ ψ.toStr ++ ")"
• (φ.or ψ).toStr = "(" ++ φ.toStr ++ " ∨ " ++ ψ.toStr ++ ")"
• (φ.imply ψ).toStr = "(" ++ φ.toStr ++ " → " ++ ψ.toStr ++ ")"
• (φ.iff ψ).toStr = "(" ++ φ.toStr ++ " ↔ " ++ ψ.toStr ++ ")"

@[implicit_reducible]

instance LO.Meta.Litform.instToString {α : Type u_1} [ToString α] : ToString (Litform α)

Equations

• LO.Meta.Litform.instToString = { toString := LO.Meta.Litform.toStr }

def LO.Meta.Litform.format {α : Type u_1} [Repr α] : Litform α → Std.Format

Equations

• LO.Meta.Litform.verum.format = Std.Format.text (toString "⊤")
• LO.Meta.Litform.falsum.format = Std.Format.text (toString "⊥")
• (LO.Meta.Litform.atom a).format = repr a
• φ.neg.format = Std.Format.text (toString "(¬" ++ toString φ.format ++ toString ")")
• (φ.and ψ).format = Std.Format.text (toString "(" ++ toString φ.format ++ toString " ∧ " ++ toString ψ.format ++ toString ")")
• (φ.or ψ).format = Std.Format.text (toString "(" ++ toString φ.format ++ toString " ∨ " ++ toString ψ.format ++ toString ")")
• (φ.imply ψ).format = Std.Format.text (toString "(" ++ toString φ.format ++ toString " → " ++ toString ψ.format ++ toString ")")
• (φ.iff ψ).format = Std.Format.text (toString "(" ++ toString φ.format ++ toString " ↔ " ++ toString ψ.format ++ toString ")")

@[implicit_reducible]

instance LO.Meta.Litform.instRepr {α : Type u_1} [Repr α] : Repr (Litform α)

Equations

• LO.Meta.Litform.instRepr = { reprPrec := fun (t : LO.Meta.Litform α) (x : ℕ) => t.format }

@[reducible, inline]

abbrev LO.Meta.Lit : Type

Equations

• LO.Meta.Lit = LO.Meta.Litform Lean.Expr

@[reducible, inline]

abbrev LO.Meta.Litform.toExpr {u_1 : Lean.Level} {F : Q(Type u_1)} (ls : Q(LogicalConnective «$F»)) : Lit → Q(«$F»)

Equations

• LO.Meta.Litform.toExpr ls (LO.Meta.Litform.atom e) = e
• LO.Meta.Litform.toExpr ls LO.Meta.Litform.verum = q(⊤)
• LO.Meta.Litform.toExpr ls LO.Meta.Litform.falsum = q(⊥)
• LO.Meta.Litform.toExpr ls (LO.Meta.Litform.and φ ψ) = let toExpr_1 := LO.Meta.Litform.toExpr ls φ; let toExpr_2 := LO.Meta.Litform.toExpr ls ψ; q(«$toExpr_1» ⋏ «$toExpr_2»)
• LO.Meta.Litform.toExpr ls (LO.Meta.Litform.or φ ψ) = let toExpr_1 := LO.Meta.Litform.toExpr ls φ; let toExpr_2 := LO.Meta.Litform.toExpr ls ψ; q(«$toExpr_1» ⋎ «$toExpr_2»)
• LO.Meta.Litform.toExpr ls (LO.Meta.Litform.neg φ) = let toExpr_1 := LO.Meta.Litform.toExpr ls φ; q(∼«$toExpr_1»)
• LO.Meta.Litform.toExpr ls (LO.Meta.Litform.imply φ ψ) = let toExpr_1 := LO.Meta.Litform.toExpr ls φ; let toExpr_2 := LO.Meta.Litform.toExpr ls ψ; q(«$toExpr_1» 🡒 «$toExpr_2»)
• LO.Meta.Litform.toExpr ls (φ.iff ψ) = let toExpr_1 := LO.Meta.Litform.toExpr ls φ; let toExpr_2 := LO.Meta.Litform.toExpr ls ψ; q(«$toExpr_1» 🡘 «$toExpr_2»)

partial def LO.Meta.Litform.summands {u : Lean.Level} {α : have u := u; Q(Type u)} (inst : Q(Add «$α»)) : Q(«$α») → Lean.MetaM (List Q(«$α»))

partial def LO.Meta.Litform.denote {u_1 : Lean.Level} {F : Q(Type u_1)} (ls : Q(LogicalConnective «$F»)) : Q(«$F») → Lean.MetaM Lit

def LO.Meta.Litform.complexity {α : Type u_1} : Litform α → ℕ

Equations

• (LO.Meta.Litform.atom a).complexity = 0
• LO.Meta.Litform.verum.complexity = 0
• LO.Meta.Litform.falsum.complexity = 0
• (φ.and ψ).complexity = max φ.complexity ψ.complexity + 1
• (φ.or ψ).complexity = max φ.complexity ψ.complexity + 1
• φ.neg.complexity = φ.complexity + 1
• (φ.imply ψ).complexity = max φ.complexity ψ.complexity + 1
• (φ.iff ψ).complexity = max φ.complexity ψ.complexity + 1

def LO.Meta.Lit.DEq : Lit → Lit → Lean.MetaM Bool

Equations

• LO.Meta.Lit.DEq (LO.Meta.Litform.atom e) (LO.Meta.Litform.atom e') = Lean.Meta.isDefEq e e'
• LO.Meta.Lit.DEq LO.Meta.Litform.verum LO.Meta.Litform.verum = pure true
• LO.Meta.Lit.DEq LO.Meta.Litform.falsum LO.Meta.Litform.falsum = pure true
• LO.Meta.Lit.DEq (LO.Meta.Litform.neg φ) (LO.Meta.Litform.neg ψ) = φ.DEq ψ
• LO.Meta.Lit.DEq (LO.Meta.Litform.and φ₁ ψ₁) (LO.Meta.Litform.and φ₂ ψ₂) = do let __do_lift ← φ₁.DEq φ₂ let __do_lift_1 ← ψ₁.DEq ψ₂ pure (__do_lift && __do_lift_1)
• LO.Meta.Lit.DEq (LO.Meta.Litform.or φ₁ ψ₁) (LO.Meta.Litform.or φ₂ ψ₂) = do let __do_lift ← φ₁.DEq φ₂ let __do_lift_1 ← ψ₁.DEq ψ₂ pure (__do_lift && __do_lift_1)
• LO.Meta.Lit.DEq (LO.Meta.Litform.imply φ₁ ψ₁) (LO.Meta.Litform.imply φ₂ ψ₂) = do let __do_lift ← φ₁.DEq φ₂ let __do_lift_1 ← ψ₁.DEq ψ₂ pure (__do_lift && __do_lift_1)
• LO.Meta.Lit.DEq (φ₁.iff ψ₁) (φ₂.iff ψ₂) = do let __do_lift ← LO.Meta.Lit.DEq φ₁ φ₂ let __do_lift_1 ← LO.Meta.Lit.DEq ψ₁ ψ₂ pure (__do_lift && __do_lift_1)
• x✝¹.DEq x✝ = pure false

def LO.Meta.Lit.dMem (φ : Lit) (Δ : List Lit) : Lean.MetaM Bool

Equations

• φ.dMem Δ = List.foldrM (fun (ψ : LO.Meta.Lit) (ih : Bool) => do let __do_lift ← φ.DEq ψ pure (__do_lift || ih)) false Δ

def LO.Meta.Lit.dSubsetList (Γ Δ : List Lit) : Lean.MetaM Bool

Equations

• LO.Meta.Lit.dSubsetList [] Δ = pure true
• LO.Meta.Lit.dSubsetList (φ :: Γ_2) Δ = do let __do_lift ← φ.dMem Γ_2 let __do_lift_1 ← LO.Meta.Lit.dSubsetList Γ_2 Δ pure (__do_lift && __do_lift_1)