Agda.ImpossibleTest

Facility to test throwing internal errors.

Synopsis

valueimpossibleTest :: (MonadDebug m, HasCallStack) => [String] -> m a

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

valueimpossibleTestReduceM :: HasCallStack => [String] -> TCM a