Agda-2.2.6: A dependently typed functional programming language and proof assistantSource codeContentsIndex
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
throwImpossible :: Impossible -> aSource
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 aSource
Catch an "impossible" error, if possible.
Produced by Haddock version 2.6.0