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

Safe Haskell | None
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

Instances details

NFData Empty Source # | Values of type `Empty` are not forced, because `Empty` is used as a constructor argument in `Substitution'`.
Instance details Defined in Agda.Utils.Empty Methods rnf :: 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 #
Eq Empty Source # |
Instance details Defined in Agda.Utils.Empty Methods (==) :: Empty -> Empty -> Bool Source # (/=) :: Empty -> Empty -> Bool 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 #

absurd :: Empty -> a Source #

toImpossible :: Empty -> IO Impossible Source #

`toImpossible e` extracts the `Impossible` value raised via `IMPOSSIBLE` 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.