Major Section: PROGRAMMING
(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
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
(error1 ctx str alist) is encountered during evaluation, then the
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