def LO.IntProp.Formula.toModalFormula {α : Type u_1} : LO.IntProp.Formula α → LO.Modal.Formula α

Equations

• LO.IntProp.Formula.atom aᴹ = LO.Modal.Formula.atom a
• LO.IntProp.Formula.verumᴹ = ⊤
• LO.IntProp.Formula.falsumᴹ = ⊥
• φ.negᴹ = ∼φᴹ
• φ.imp ψᴹ = φᴹ ➝ ψᴹ
• φ.and ψᴹ = φᴹ ⋏ ψᴹ
• φ.or ψᴹ = φᴹ ⋎ ψᴹ

def LO.IntProp.«term_ᴹ» : Lean.TrailingParserDescr

Equations

• LO.IntProp.«term_ᴹ» = Lean.ParserDescr.trailingNode `LO.IntProp.«term_ᴹ» 75 75 (Lean.ParserDescr.symbol "ᴹ")

def LO.Modal.Formula.toPropFormula {α : Type u_1} (φ : LO.Modal.Formula α) : autoParam (φ.degree = 0) _auto✝ → LO.IntProp.Formula α

Equations

• (LO.Modal.Formula.atom aᴾ) x_1 = LO.IntProp.Formula.atom a
• (LO.Modal.Formula.falsumᴾ) x_1 = ⊥
• (φ_2.imp ψᴾ) x_1 = (φ_2ᴾ) ⋯ ➝ (ψᴾ) ⋯

def LO.Modal.«term_ᴾ» : Lean.TrailingParserDescr

Equations

• LO.Modal.«term_ᴾ» = Lean.ParserDescr.trailingNode `LO.Modal.«term_ᴾ» 75 75 (Lean.ParserDescr.symbol "ᴾ")