print an error message and stop execution
Major Section:  ACL2-BUILT-INS

(Illegal 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, and see prog2$ for an example of how to use a related function, hard-error (see hard-error). Also see er for a macro that provides a unified way of signaling errors.

The difference between illegal and hard-error is that the former has a guard of nil while the latter has a guard of t. Thus, you may want to use illegal rather than hard-error when you intend to do guard verification at some point, and you expect the guard to guarantee that the illegal call is never executed. See prog2$ for an example.