equational-reasoning-0.2.0.5: Proof assistant for Haskell using DataKinds & PolyKinds

Safe HaskellSafe-Inferred
LanguageHaskell98

Proof.Propositional

Description

Provides type synonyms for logical connectives.

Documentation

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