equational-reasoning-0.2.0.7: Proof assistant for Haskell using DataKinds & PolyKinds
Proof.Propositional
Description
Provides type synonyms for logical connectives.
type (/\) a b = (a, b) infixr 3 Source
type (\/) a b = Either a b infixr 2 Source
type Not a = a -> Void Source
exfalso :: a -> Not a -> b Source
orIntroL :: a -> a \/ b Source
orIntroR :: b -> a \/ b Source
orElim :: (a \/ b) -> (a -> c) -> (b -> c) -> c Source
andIntro :: a -> b -> a /\ b Source
andElimL :: (a /\ b) -> a Source
andElimR :: (a /\ b) -> b Source
orAssocL :: (a \/ (b \/ c)) -> (a \/ b) \/ c Source
orAssocR :: ((a \/ b) \/ c) -> a \/ (b \/ c) Source
andAssocL :: (a /\ (b /\ c)) -> (a /\ b) /\ c Source
andAssocR :: ((a /\ b) /\ c) -> a /\ (b /\ c) Source