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.
