Agda
Safe HaskellNone
LanguageHaskell2010

Agda.Utils.Empty

Description

An empty type with some useful instances.

Synopsis

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 -> () #

Show Empty Source # 
Instance details

Defined in Agda.Utils.Empty

Methods

showsPrec :: Int -> Empty -> ShowS #

show :: Empty -> String #

showList :: [Empty] -> ShowS #

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.