Documentation

Foundation.Modal.IntProp

source
def LO.IntProp.Formula.toModalFormula {α : Type u_1} :
Formula α → Modal.Formula α
Equations
Instances For
    source
    def LO.IntProp.«term_ᴹ» :
    Lean.TrailingParserDescr
    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) _auto✝ → IntProp.Formula α
      Equations
      Instances For
        source
        def LO.Modal.«term_ᴾ» :
        Lean.TrailingParserDescr
        Equations
        Instances For