Agda-2.2.4: 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

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