Agda-2.6.0.1: A dependently typed functional programming language and proof assistant

Safe Haskell | Safe
Language | Haskell2010

Agda.Utils.Empty

Description

An empty type with some useful instances.

Synopsis

- data Empty
- absurd :: Empty -> a
- toImpossible :: Empty -> IO Impossible

# Documentation

data Empty Source #

Instances

Eq Empty Source # |
Instance details Defined in Agda.Utils.Empty Methods (==) :: Empty -> Empty -> Bool Source # (/=) :: Empty -> Empty -> Bool Source #
Data Empty Source # |

Instance details

Defined in Agda.Utils.Empty

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Empty -> c Empty Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Empty Source #

toConstr :: Empty -> Constr Source #

dataTypeOf :: Empty -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Empty) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Empty) Source #

gmapT :: (forall b. Data b => b -> b) -> Empty -> Empty Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Empty -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Empty -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Empty -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Empty -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Empty -> m Empty Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Empty -> m Empty Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Empty -> m Empty Source #

Ord Empty Source # |
Instance details Defined in Agda.Utils.Empty Methods compare :: Empty -> Empty -> Ordering Source # (<) :: Empty -> Empty -> Bool Source # (<=) :: Empty -> Empty -> Bool Source # (>) :: Empty -> Empty -> Bool Source # (>=) :: Empty -> Empty -> Bool Source # max :: Empty -> Empty -> Empty Source # min :: Empty -> Empty -> Empty Source #
Show Empty Source # |
Instance details Defined in Agda.Utils.Empty Methods showsPrec :: Int -> Empty -> ShowS Source # show :: Empty -> String Source # showList :: [Empty] -> ShowS Source #
EmbPrj Empty Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Common Methods icode :: Empty -> S Int32 Source # icod_ :: Empty -> S Int32 Source # value :: Int32 -> R Empty Source #

absurd :: Empty -> a Source #

toImpossible :: Empty -> IO Impossible Source #

`toImpossible e` extracts the `Impossible` value raised via `(throwImpossible (Impossible "srcfullAgdaUtilsEmpty.hs" 33))` to create the element `e` of type `Empty`. It proceeds by evaluating `e` to weak head normal form and catching the exception. We are forced to wrap things in a `Maybe` because of `catchImpossible`'s type.