Major Section: ACL2-BUILT-INS
(Hard-error ctx str alist) causes evaluation to halt with a short
message using the ``context'' ctx. An error message is first printed
using the string str and alist alist that are of the same kind
as expected by fmt. See fmt. Also see er for a macro that provides a
unified way of signaling errors.
Hard-error has a guard of t. Also see illegal for a
similar capability which however has a guard of nil that supports
static checking using guard verification, rather than using dynamic
(run-time) checking. This distinction is illustrated elsewhere:
see prog2$ for examples.
Semantically, hard-error ignores its arguments and always returns
nil. But if a call (hard-error ctx str alist) is encountered
during evaluation, then the string str is printed using the
association list alist (as in fmt), after which evaluation halts
immediately. Here is a trivial, contrived example.
ACL2 !>(cons 3 (hard-error 'my-context
"Printing 4: ~n0"
(list (cons #\0 4))))
HARD ACL2 ERROR in MY-CONTEXT: Printing 4: four
ACL2 Error in TOP-LEVEL: Evaluation aborted.
ACL2 !>
