Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Proof.Propositional
Contents
Description
Provides type synonyms for logical connectives.
Synopsis
- type (/\) a b = (a, b)
- type (\/) a b = Either a b
- 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)
- data IsTrue (b :: Bool) where
- withWitness :: forall b r. IsTrue b -> (b ~ 'True => r) -> r
- class Empty a where
- eliminate :: a -> x
- withEmpty :: forall a b. (a -> Void) -> (Empty a => b) -> b
- withEmpty' :: forall a b. (forall c. a -> c) -> (Empty a => b) -> b
- refute :: TypeQ -> DecsQ
- class Inhabited a where
- trivial :: a
- withInhabited :: forall a b. a -> (Inhabited a => b) -> b
- prove :: TypeQ -> DecsQ
Documentation
data IsTrue (b :: Bool) where Source #
Utility type to convert type-level (
-valued) predicate function
into concrete witness data-type.Bool
Instances
Data (IsTrue 'True) Source # | |
Defined in Proof.Propositional Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> IsTrue 'True -> c (IsTrue 'True) # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (IsTrue 'True) # toConstr :: IsTrue 'True -> Constr # dataTypeOf :: IsTrue 'True -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (IsTrue 'True)) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (IsTrue 'True)) # gmapT :: (forall b. Data b => b -> b) -> IsTrue 'True -> IsTrue 'True # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> IsTrue 'True -> r # gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> IsTrue 'True -> r # gmapQ :: (forall d. Data d => d -> u) -> IsTrue 'True -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> IsTrue 'True -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> IsTrue 'True -> m (IsTrue 'True) # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> IsTrue 'True -> m (IsTrue 'True) # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> IsTrue 'True -> m (IsTrue 'True) # | |
Read (IsTrue 'True) Source # | |
Show (IsTrue b) Source # | |
Empty (IsTrue 'False) Source # | |
Inhabited (IsTrue 'True) Source # | |
Eq (IsTrue b) Source # | |
Ord (IsTrue b) Source # | |
Defined in Proof.Propositional |
Type-class for types without inhabitants, dual to
.
Current GHC doesn't provide selective-instance,
hence we don't Inhabited
provide instances
for product types in a generic deriving (DeriveAnyClass).Empty
To derive an instance for each concrete types,
use
.refute
Since 0.4.0.0.
Minimal complete definition
Nothing
Methods
Instances
Empty Void Source # | |
Defined in Proof.Propositional.Empty | |
Empty (IsTrue 'False) Source # | |
(Empty a, Empty b) => Empty (Either a b) Source # | |
Defined in Proof.Propositional.Empty | |
(Inhabited a, Empty b) => Empty (a -> b) Source # | |
Defined in Proof.Propositional | |
Empty ('EQ :~: 'GT) Source # | |
Empty ('EQ :~: 'LT) Source # | |
Empty ('GT :~: 'EQ) Source # | |
Empty ('GT :~: 'LT) Source # | |
Empty ('LT :~: 'EQ) Source # | |
Empty ('LT :~: 'GT) Source # | |
Empty (0 :~: 1) Source # | |
Defined in Proof.Propositional | |
Empty ('False :~: 'True) Source # | |
Empty ('True :~: 'False) Source # | |
Empty (() :~: Int) Source # | |
withEmpty :: forall a b. (a -> Void) -> (Empty a => b) -> b Source #
Giving falsity witness by proving
from Void
a
.
See also withEmpty'
.
Since 0.4.0.0
withEmpty' :: forall a b. (forall c. a -> c) -> (Empty a => b) -> b Source #
Giving falsity witness by showing a
entails everything.
See also withEmpty
.
Since 0.4.0.0
refute :: TypeQ -> DecsQ Source #
Macro to automatically derive
instance for
concrete (variable-free) types which may contain products.Empty
class Inhabited a where Source #
Types with at least one inhabitant, dual to
.
Currently, GHC doesn't provide a selective-instance,
hence we can't generically derive Empty
instances
for sum types (i.e. by Inhabited
DeriveAnyClass
).
To derive an instance for each concrete types,
use
.prove
Since 0.4.0.0.
Minimal complete definition
Nothing
Methods
A generic inhabitant of type
, which means that
one cannot assume anything about the value of a
except that ittrivial
- is of type
a
, and - doesn't contain any partial values.
Instances
withInhabited :: forall a b. a -> (Inhabited a => b) -> b Source #
prove :: TypeQ -> DecsQ Source #
Macro to automatically derive
instance for
concrete (variable-free) types which may contain sums.Inhabited
Orphan instances
Inhabited Ordering Source # | |
Inhabited Integer Source # | |
Inhabited Bool Source # | |
Inhabited Char Source # | |
Inhabited Double Source # | |
Inhabited Float Source # | |
Inhabited Int Source # | |
Inhabited Word Source # | |
Inhabited (Ratio Integer) Source # | |
Inhabited (Maybe a) Source # | |
Inhabited [a] Source # | |
(Inhabited a, Empty b) => Empty (a -> b) Source # | |
Empty ('EQ :~: 'GT) Source # | |
Empty ('EQ :~: 'LT) Source # | |
Empty ('GT :~: 'EQ) Source # | |
Empty ('GT :~: 'LT) Source # | |
Empty ('LT :~: 'EQ) Source # | |
Empty ('LT :~: 'GT) Source # | |
Empty (0 :~: 1) Source # | |
Empty ('False :~: 'True) Source # | |
Empty ('True :~: 'False) Source # | |
Empty (() :~: Int) Source # | |
Inhabited (n :~: n) Source # | |