Proof.Propositional

Provides type synonyms for logical connectives.

Documentation

type (/\) a b = (a, b) infixr 3

type (\/) a b = Either a b infixr 2

type Not a = a -> Void

exfalso :: a -> Not a -> b

orIntroL :: a -> a \/ b

orIntroR :: b -> a \/ b

orElim :: (a \/ b) -> (a -> c) -> (b -> c) -> c

andIntro :: a -> b -> a /\ b

andElimL :: (a /\ b) -> a

andElimR :: (a /\ b) -> b

orAssocL :: (a \/ (b \/ c)) -> (a \/ b) \/ c

orAssocR :: ((a \/ b) \/ c) -> a \/ (b \/ c)

andAssocL :: (a /\ (b /\ c)) -> (a /\ b) /\ c

andAssocR :: ((a /\ b) /\ c) -> a /\ (b /\ c)