Agda-2.6.2.2: A dependently typed functional programming language and proof assistant

Safe Haskell | Safe-Inferred
Language | Haskell2010

Agda.Interaction.ExitCode

Synopsis

- data AgdaError
  - = UnknownError
  - | TCMError
  - | OptionError
  - | ImpossibleError
- agdaErrorToInt :: AgdaError -> Int
- agdaErrorFromInt :: Int -> Maybe AgdaError
- exitSuccess :: IO a
- exitAgdaWith :: AgdaError -> IO ()

# Documentation

data AgdaError Source #

Constructors

UnknownError | 1
TCMError | 42
OptionError | 71
ImpossibleError | 154

#### Instances

Instances details

Bounded AgdaError Source # |
Instance details Defined in Agda.Interaction.ExitCode Methods minBound :: AgdaError Source # maxBound :: AgdaError Source #
Enum AgdaError Source # |

Instance details

Defined in Agda.Interaction.ExitCode

Methods

succ :: AgdaError -> AgdaError Source #

pred :: AgdaError -> AgdaError Source #

toEnum :: Int -> AgdaError Source #

fromEnum :: AgdaError -> Int Source #

enumFrom :: AgdaError -> [AgdaError] Source #

enumFromThen :: AgdaError -> AgdaError -> [AgdaError] Source #

enumFromTo :: AgdaError -> AgdaError -> [AgdaError] Source #

enumFromThenTo :: AgdaError -> AgdaError -> AgdaError -> [AgdaError] Source #

Show AgdaError Source # |
Instance details Defined in Agda.Interaction.ExitCode Methods showsPrec :: Int -> AgdaError -> ShowS Source # show :: AgdaError -> String Source # showList :: [AgdaError] -> ShowS Source #
Eq AgdaError Source # |
Instance details Defined in Agda.Interaction.ExitCode Methods (==) :: AgdaError -> AgdaError -> Bool Source # (/=) :: AgdaError -> AgdaError -> Bool Source #

agdaErrorToInt :: AgdaError -> Int Source #

Return the error corresponding to an exit code from the Agda process

agdaErrorFromInt :: Int -> Maybe AgdaError Source #

exitSuccess :: IO a Source #

The computation `exitSuccess` is equivalent to `exitWith` `ExitSuccess`, It terminates the program successfully.

exitAgdaWith :: AgdaError -> IO () Source #