| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

Agda.Utils.Impossible

Description
An interface for reporting "impossible" errors
Synopsis

data Impossible = Impossible String Integer
throwImpossible :: Impossible -> a
catchImpossible :: IO a -> (Impossible -> IO a) -> IO a

Documentation

data Impossible | Source

"Impossible" errors, annotated with a file name and a line number corresponding to the source code location of the error.
Constructors

Impossible String Integer |

Instances

Show Impossible
Typeable Impossible
Exception Impossible

throwImpossible :: Impossible -> a | Source

Abort by throwing an "impossible" error. You should not use this function directly. Instead use the macro in `undefined.h`.

catchImpossible :: IO a -> (Impossible -> IO a) -> IO a | Source

Catch an "impossible" error, if possible.
Produced by Haddock version 2.4.2