HARD-ERROR

print an error message and stop execution
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 !>