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,
(see hard-error). Also see er for a macro that provides a unified
way of signaling errors.
The difference between
hard-error is that the former
has a guard of
nil while the latter has a
you may want to use
illegal rather than
hard-error when you intend
guard verification at some point, and you expect the guard
to guarantee that the
illegal call is never executed.
See prog2$ for an example.