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

Safe Haskell | None
Language | Haskell2010

Agda.ImpossibleTest

Description

Facility to test throwing internal errors.

Synopsis

- impossibleTest :: (MonadDebug m, HasCallStack) => [String] -> m a
- impossibleTestReduceM :: HasCallStack => [String] -> TCM a

# Documentation

impossibleTest :: (MonadDebug m, HasCallStack) => [String] -> m a Source #

If the given list of words is non-empty, print them as debug message (using `__IMPOSSIBLE_VERBOSE__`) before raising the internal error.

impossibleTestReduceM :: HasCallStack => [String] -> TCM a Source #