Major Section: PROGRAMMING (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