be generalised outside the PL scope, once we have typeclasses to express that a type possesses an
implication connective.
|
/-- An inference system is classical if it validates double-negation elimination. TODO: this should |
|
be generalised outside the `PL` scope, once we have typeclasses to express that a type possesses an |
|
implication connective. -/ |
be generalised outside the
PLscope, once we have typeclasses to express that a type possesses animplication connective.
cslib/Cslib/Logics/Propositional/Defs.lean
Lines 132 to 134 in 70c5bf5