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.
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
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 !>