ModuleAgda-2.8.0.2Haskell2010

Agda.Utils.Empty

An empty type with some useful instances.

Synopsis

data Empty
value absurd
value toImpossible

PackageAgda-2.8.0.2
Exports3
LanguageHaskell2010
LicenceMIT
SourceEmpty.hs

datadata Empty

Instances4Eq, Ord, Show, NFData

Eq EmptyDefined in Agda-2.8.0.2 · Agda.Utils.Empty
Ord EmptyDefined in Agda-2.8.0.2 · Agda.Utils.Empty
Show EmptyDefined in Agda-2.8.0.2 · Agda.Utils.Empty
NFData EmptyDefined in Agda-2.8.0.2 · Agda.Utils.Empty
Values of type Empty are not forced, because Empty is used as a constructor argument in Substitution'.

valueabsurd :: Empty -> a

valuetoImpossible :: 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.