Safe Haskell	Safe-Inferred
Language	Haskell2010

Agda.Utils.Empty

Description

An empty type with some useful instances.

Synopsis

Documentation

data Empty Source #

Instances

Instances details

Show Empty Source #
Instance details Defined in Agda.Utils.Empty Methods showsPrec :: Int -> Empty -> ShowS # show :: Empty -> String # showList :: [Empty] -> ShowS #
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 -> () #
Eq Empty Source #
Instance details Defined in Agda.Utils.Empty Methods (==) :: Empty -> Empty -> Bool # (/=) :: Empty -> Empty -> Bool #
Ord Empty Source #
Instance details Defined in Agda.Utils.Empty Methods compare :: Empty -> Empty -> Ordering # (<) :: Empty -> Empty -> Bool # (<=) :: Empty -> Empty -> Bool # (>) :: Empty -> Empty -> Bool # (>=) :: Empty -> Empty -> Bool # max :: Empty -> Empty -> Empty # min :: Empty -> Empty -> Empty #

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.