Safe Haskell | None |
---|---|
Language | Haskell2010 |
Documentation
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.
Nothing
Instances
Empty Void Source # | |
Defined in Proof.Propositional.Empty | |
Empty (IsTrue False) Source # | |
(Inhabited a, Empty b) => Empty (a -> b) Source # | |
Defined in Proof.Propositional | |
(Empty a, Empty b) => Empty (Either a b) Source # | |
Defined in Proof.Propositional.Empty | |
Empty (False :~: True) Source # | |
Empty (True :~: False) Source # | |
Empty (LT :~: EQ) Source # | |
Empty (LT :~: GT) Source # | |
Empty (EQ :~: LT) Source # | |
Empty (EQ :~: GT) Source # | |
Empty (GT :~: LT) Source # | |
Empty (GT :~: EQ) Source # | |
Empty (() :~: Int) Source # | |
Empty (0 :~: 1) Source # | |
Defined in Proof.Propositional |
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