generalised outside the PL scope, once we have typeclasses to express that a type possesses an
implication connective.
|
/-- An inference system is intuitionistic if it derives ex falso quodlibet. TODO: this should be |
|
generalised outside the `PL` scope, once we have typeclasses to express that a type possesses an |
|
implication connective. -/ |
generalised outside the
PLscope, once we have typeclasses to express that a type possesses animplication connective.
cslib/Cslib/Logics/Propositional/Defs.lean
Lines 123 to 125 in 70c5bf5