Error1
Print an error message and cause a ``soft error''
(Error1 ctx summary str alist state) returns (mv t nil
state). An error message is first printed using the ``context'' ctx,
as well as the string str and alist alist that are of the same kind
as expected by fmt — unless error output is inhibited
(see set-inhibit-output-lst and with-output) or summary is
non-nil, in which case it is a string, and error output of that type is
inhibited (see set-inhibit-er). See fmt.
Error1 can be interpreted as causing an ``error'' when programming
with the ACL2 state, something most ACL2 users will probably not want
to do; see ld-error-triples and see er-progn. In order to cause
errors with :logic mode functions, see hard-error and see
illegal. Better yet, see er for a macro that provides a unified
way of signaling errors.
As mentioned above, error1 always returns (mv t nil state). But
if a call (error1 ctx summary str alist) is encountered during
evaluation, then unless output is inhibited as described above, the string
str is first printed using the association list alist (as in fmt). Here is a trivial, contrived example.
ACL2 !>(error1 'my-context
"Printing 4: ~n0"
(list (cons #\0 4))
state)
ACL2 Error in MY-CONTEXT: Printing 4: four
ACL2 !>
