Agda-2.7.0: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.ImpossibleTest

Description

Facility to test throwing internal errors.

Synopsis

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.