def LO.Propositional.Superintuitionistic.Formula.toClassical {α : Type u_1} : LO.Propositional.Superintuitionistic.Formula α → LO.Propositional.Classical.Formula α

Equations

• (LO.Propositional.Superintuitionistic.Formula.atom a).toClassical = LO.Propositional.Classical.Formula.atom a
• LO.Propositional.Superintuitionistic.Formula.verum.toClassical = ⊤
• LO.Propositional.Superintuitionistic.Formula.falsum.toClassical = ⊥
• p.neg.toClassical = ~p.toClassical
• (p.and q).toClassical = p.toClassical ⋏ q.toClassical
• (p.or q).toClassical = p.toClassical ⋎ q.toClassical
• (p.imp q).toClassical = p.toClassical ⟶ q.toClassical

instance LO.Propositional.Superintuitionistic.instCoeFormulaFormula {α : Type u_1} : Coe (LO.Propositional.Superintuitionistic.Formula α) (LO.Propositional.Classical.Formula α)

Equations

• LO.Propositional.Superintuitionistic.instCoeFormulaFormula = { coe := LO.Propositional.Superintuitionistic.Formula.toClassical }

instance LO.Propositional.Superintuitionistic.instCoeTheoryTheory {α : Type u_1} : Coe (LO.Propositional.Superintuitionistic.Theory α) (LO.Propositional.Classical.Theory α)

Equations

• One or more equations did not get rendered due to their size.

def LO.Propositional.Classical.Formula.toSuperintuitionistic {α : Type u_1} : LO.Propositional.Classical.Formula α → LO.Propositional.Superintuitionistic.Formula α

Equations

• (LO.Propositional.Classical.Formula.atom a).toSuperintuitionistic = LO.Propositional.Superintuitionistic.Formula.atom a
• (LO.Propositional.Classical.Formula.natom a).toSuperintuitionistic = ~LO.Propositional.Superintuitionistic.Formula.atom a
• LO.Propositional.Classical.Formula.verum.toSuperintuitionistic = ⊤
• LO.Propositional.Classical.Formula.falsum.toSuperintuitionistic = ⊥
• (p.and q).toSuperintuitionistic = p.toSuperintuitionistic ⋏ q.toSuperintuitionistic
• (p.or q).toSuperintuitionistic = p.toSuperintuitionistic ⋎ q.toSuperintuitionistic

instance LO.Propositional.Classical.instCoeFormulaFormula {α : Type u_1} : Coe (LO.Propositional.Classical.Formula α) (LO.Propositional.Superintuitionistic.Formula α)

Equations

• LO.Propositional.Classical.instCoeFormulaFormula = { coe := LO.Propositional.Classical.Formula.toSuperintuitionistic }

instance LO.Propositional.Classical.instCoeTheoryTheory {α : Type u_1} : Coe (LO.Propositional.Classical.Theory α) (LO.Propositional.Superintuitionistic.Theory α)

Equations

• LO.Propositional.Classical.instCoeTheoryTheory = { coe := fun (x : LO.Propositional.Classical.Theory α) => LO.Propositional.Classical.Formula.toSuperintuitionistic '' x }