To string for LZFC.Term and LZFC.BoundedFormula

Converts terms and bounded formulas in the language LZFC to readable strings, with two flavors (with and without depth information).

def FirstOrder.ZFC.TermToString {α : Type u_1} [ToString α] {n : ℕ} (t : Language.LZFC.Term (α ⊕ Fin n)) : String

Converts a term into a string.

Equations

• FirstOrder.ZFC.TermToString (FirstOrder.Language.var (Sum.inl a)) = toString "fv" ++ toString (toString a)
• FirstOrder.ZFC.TermToString (FirstOrder.Language.var (Sum.inr k)) = toString "bv" ++ toString k
• FirstOrder.ZFC.TermToString t = "error"

def FirstOrder.ZFC.TermTupleToString {α : Type u_1} [ToString α] {n m : ℕ} (ts : Fin m → Language.LZFC.Term (α ⊕ Fin n)) (k : ℕ) : String

Converts a tuple of terms into a string.

Equations

• FirstOrder.ZFC.TermTupleToString ts_2 k = "error"
• FirstOrder.ZFC.TermTupleToString ts_2 k = FirstOrder.ZFC.TermToString (ts_2 (Fin.ofNat (m' + 1) k))

def FirstOrder.ZFC.FormulaToString {α : Type u_1} [ToString α] {n : ℕ} (ϕ : Language.LZFC.BoundedFormula α n) : String

Converts a formula into a string.

Equations

• One or more equations did not get rendered due to their size.
• FirstOrder.ZFC.FormulaToString FirstOrder.Language.BoundedFormula.falsum = "⊥"
• FirstOrder.ZFC.FormulaToString ϕ1.all = toString "∀'bv" ++ toString n ++ toString "(" ++ toString (FirstOrder.ZFC.FormulaToString ϕ1) ++ toString ")"
• FirstOrder.ZFC.FormulaToString (ϕ1.imp FirstOrder.Language.BoundedFormula.falsum) = toString "∼" ++ toString (FirstOrder.ZFC.FormulaToString ϕ1)
• FirstOrder.ZFC.FormulaToString (FirstOrder.Language.BoundedFormula.equal t1 t2) = toString (FirstOrder.ZFC.TermToString t1) ++ toString " = " ++ toString (FirstOrder.ZFC.TermToString t2)
• FirstOrder.ZFC.FormulaToString (ϕ1.imp ϕ2) = toString (FirstOrder.ZFC.FormulaToString ϕ1) ++ toString " ⟹ " ++ toString (FirstOrder.ZFC.FormulaToString ϕ2)

def FirstOrder.ZFC.TermToString' {n : ℕ} (t : Language.LZFC.Term (ℕ ⊕ Fin n)) : String

Converts a term into a string with depth

Equations

• FirstOrder.ZFC.TermToString' (FirstOrder.Language.var (Sum.inl k)) = toString "fv " ++ toString n ++ toString " " ++ toString k
• FirstOrder.ZFC.TermToString' (FirstOrder.Language.var (Sum.inr k)) = toString "bv " ++ toString n ++ toString " " ++ toString k
• FirstOrder.ZFC.TermToString' t = "error"

def FirstOrder.ZFC.TermPairFirstToString' {n m : ℕ} (ts : Fin m → Language.LZFC.Term (ℕ ⊕ Fin n)) : String

Converts the first term of a pair into a string with depth

Equations

• FirstOrder.ZFC.TermPairFirstToString' ts_2 = FirstOrder.ZFC.TermToString' (ts_2 0)
• FirstOrder.ZFC.TermPairFirstToString' ts = ""

def FirstOrder.ZFC.TermPairSecondToString' {n m : ℕ} (ts : Fin m → Language.LZFC.Term (ℕ ⊕ Fin n)) : String

Converts the second term of a pair into a string with depth

Equations

• FirstOrder.ZFC.TermPairSecondToString' ts_2 = FirstOrder.ZFC.TermToString' (ts_2 1)
• FirstOrder.ZFC.TermPairSecondToString' ts = ""

def FirstOrder.ZFC.FormulaToString' {n : ℕ} (ϕ : Language.LZFC.BoundedFormula ℕ n) : String

Converts a formula into a string with depath

Equations

• One or more equations did not get rendered due to their size.
• FirstOrder.ZFC.FormulaToString' FirstOrder.Language.BoundedFormula.falsum = "⊥"
• FirstOrder.ZFC.FormulaToString' ϕ1.all = toString "∀'bv" ++ toString n ++ toString "(" ++ toString (FirstOrder.ZFC.FormulaToString' ϕ1) ++ toString ")"
• FirstOrder.ZFC.FormulaToString' (ϕ1.imp FirstOrder.Language.BoundedFormula.falsum) = toString "∼" ++ toString (FirstOrder.ZFC.FormulaToString' ϕ1)
• FirstOrder.ZFC.FormulaToString' (FirstOrder.Language.BoundedFormula.equal t1 t2) = toString (FirstOrder.ZFC.TermToString' t1) ++ toString " = " ++ toString (FirstOrder.ZFC.TermToString' t2)