Documentation

Foundation.Propositional.Classical.Basic.Formula

Equations
Instances For
    Equations
    • LO.Propositional.Classical.Formula.instLogicalConnective = LO.LogicalConnective.mk
    Equations
    Instances For
      Equations
      Equations
      • LO.Propositional.Classical.Formula.instToString = { toString := LO.Propositional.Classical.Formula.toStr }
      Equations
      • LO.Propositional.Classical.Formula.instDeMorgan = { verum := , falsum := , imply := , and := , or := , neg := }
      Equations
      Instances For
        @[simp]
        @[simp]
        @[simp]
        theorem LO.Propositional.Classical.Formula.complexity_and {α : Type u} (p : LO.Propositional.Classical.Formula α) (q : LO.Propositional.Classical.Formula α) :
        (p q).complexity = max p.complexity q.complexity + 1
        @[simp]
        theorem LO.Propositional.Classical.Formula.complexity_and' {α : Type u} (p : LO.Propositional.Classical.Formula α) (q : LO.Propositional.Classical.Formula α) :
        (p.and q).complexity = max p.complexity q.complexity + 1
        @[simp]
        theorem LO.Propositional.Classical.Formula.complexity_or {α : Type u} (p : LO.Propositional.Classical.Formula α) (q : LO.Propositional.Classical.Formula α) :
        (p q).complexity = max p.complexity q.complexity + 1
        @[simp]
        theorem LO.Propositional.Classical.Formula.complexity_or' {α : Type u} (p : LO.Propositional.Classical.Formula α) (q : LO.Propositional.Classical.Formula α) :
        (p.or q).complexity = max p.complexity q.complexity + 1
        def LO.Propositional.Classical.Formula.cases' {α : Type u} {C : LO.Propositional.Classical.Formula αSort w} (hverum : C ) (hfalsum : C ) (hatom : (a : α) → C (LO.Propositional.Classical.Formula.atom a)) (hnatom : (a : α) → C (LO.Propositional.Classical.Formula.natom a)) (hand : (p q : LO.Propositional.Classical.Formula α) → C (p q)) (hor : (p q : LO.Propositional.Classical.Formula α) → C (p q)) (p : LO.Propositional.Classical.Formula α) :
        C p
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          def LO.Propositional.Classical.Formula.rec' {α : Type u} {C : LO.Propositional.Classical.Formula αSort w} (hverum : C ) (hfalsum : C ) (hatom : (a : α) → C (LO.Propositional.Classical.Formula.atom a)) (hnatom : (a : α) → C (LO.Propositional.Classical.Formula.natom a)) (hand : (p q : LO.Propositional.Classical.Formula α) → C pC qC (p q)) (hor : (p q : LO.Propositional.Classical.Formula α) → C pC qC (p q)) (p : LO.Propositional.Classical.Formula α) :
          C p
          Equations
          Instances For
            @[simp]
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              Equations
              • LO.Propositional.Classical.Formula.instDecidableEq = LO.Propositional.Classical.Formula.hasDecEq
              @[reducible, inline]
              Equations
              Instances For
                Equations
                • LO.Propositional.Classical.instCollectionFormulaTheory = inferInstance