Documentation

LeanPool.Incompleteness.Foundation.Modal.IntProp

IntProp #

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

Imported declaration from the Incompleteness formalization.

Equations
Instances For
    source
    def LO.IntProp.«term_ᴹ» :
    Lean.TrailingParserDescr

    Imported declaration from the Incompleteness formalization.

    Equations
    Instances For
      source
      @[simp]
      theorem LO.IntProp.Formula.toModalFormula.def_top {α : Type u_1} :
      ⊤ᴹ = ⊤
      source
      @[simp]
      theorem LO.IntProp.Formula.toModalFormula.def_bot {α : Type u_1} :
      ⊥ᴹ = ⊥
      source
      @[simp]
      theorem LO.IntProp.Formula.toModalFormula.def_atom {α : Type u_1} (a : α) :
      atom aᴹ = Modal.Formula.atom a
      source
      @[simp]
      theorem LO.IntProp.Formula.toModalFormula.def_not {α : Type u_1} (φ : Formula α) :
      (∼φ)ᴹ = ∼φᴹ
      source
      @[simp]
      theorem LO.IntProp.Formula.toModalFormula.def_imp {α : Type u_1} (φ ψ : Formula α) :
      (φ ==> ψ)ᴹ = φᴹ ==> ψᴹ
      source
      @[simp]
      theorem LO.IntProp.Formula.toModalFormula.def_and {α : Type u_1} (φ ψ : Formula α) :
      (φ ⋏ ψ)ᴹ = φᴹ ⋏ ψᴹ
      source
      @[simp]
      theorem LO.IntProp.Formula.toModalFormula.def_or {α : Type u_1} (φ ψ : Formula α) :
      (φ ⋎ ψ)ᴹ = φᴹ ⋎ ψᴹ
      source
      def LO.Modal.Formula.toPropFormula {α : Type u_1} (φ : Formula α) :
      autoParam (φ.degree = 0) toPropFormula._auto_1 → IntProp.Formula α

      Imported declaration from the Incompleteness formalization.

      Equations
      Instances For
        source
        def LO.Modal.«term_ᴾ» :
        Lean.TrailingParserDescr

        Imported declaration from the Incompleteness formalization.

        Equations
        Instances For