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

• atom: {α : Type u_1} → α → LO.Litform α
• verum: {α : Type u_1} → LO.Litform α
• falsum: {α : Type u_1} → LO.Litform α
• and: {α : Type u_1} → LO.Litform α → LO.Litform α → LO.Litform α
• or: {α : Type u_1} → LO.Litform α → LO.Litform α → LO.Litform α
• neg: {α : Type u_1} → LO.Litform α → LO.Litform α
• imply: {α : Type u_1} → LO.Litform α → LO.Litform α → LO.Litform α

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

Equations

• LO.Litform.instLogicalConnective = LO.LogicalConnective.mk

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

Equations

• LO.Litform.verum.toStr = "⊤"
• LO.Litform.falsum.toStr = "⊥"
• (LO.Litform.atom a).toStr = toString a
• p.neg.toStr = "(¬" ++ p.toStr ++ ")"
• (p.and q).toStr = "(" ++ p.toStr ++ " ∧ " ++ q.toStr ++ ")"
• (p.or q).toStr = "(" ++ p.toStr ++ " ∨ " ++ q.toStr ++ ")"
• (p.imply q).toStr = "(" ++ p.toStr ++ " ⟶ " ++ q.toStr ++ ")"

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

Equations

• LO.Litform.instRepr = { reprPrec := fun (t : LO.Litform α) (x : ℕ) => Std.Format.text t.toStr }

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

Equations

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

@[reducible, inline]

abbrev LO.Litform.Meta.Lit {u_2 : Lean.Level} (F : Q(Type u_2)) : Type

Equations

• LO.Litform.Meta.Lit F = LO.Litform Q(«$F»)

@[reducible, inline]

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

Equations

• One or more equations did not get rendered due to their size.
• LO.Litform.Meta.toExpr F ls (LO.Litform.atom e) = q(«$e»)
• LO.Litform.Meta.toExpr F ls LO.Litform.verum = q(⊤)
• LO.Litform.Meta.toExpr F ls LO.Litform.falsum = q(⊥)
• LO.Litform.Meta.toExpr F ls (LO.Litform.neg p) = let a := LO.Litform.Meta.toExpr F ls p; let toExpr_1 := LO.Litform.Meta.toExpr F ls p; q(~«$toExpr_1»)

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

instance LO.Litform.Meta.denotation {u_1 : Lean.Level} (F : Q(Type u_1)) (ls : Q(LO.LogicalConnective «$F»)) : Denotation q(«$F») (LO.Litform.Meta.Lit F)

Equations

• LO.Litform.Meta.denotation F ls = { denote' := LO.Litform.Meta.denote F ls, toExpr' := LO.Litform.Meta.toExpr F ls }

@[reducible, inline]

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

Equations

• LO.Litform.Meta.DEq F ls p q = Denotation.DEq F p q