Major Section: ACL2-BUILT-INS
(Error1 ctx str alist) returns (mv t nil state). An error message is
first printed using the the ``context'' ctx, as well as the string
str and alist alist that are of the same kind as expected by
fmt. 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 str alist) is encountered during evaluation, then 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 !>
