Major Section: PROGRAMMING
Example Forms: (er hard 'top-level "Illegal inputs, ~x0 and ~x1." a b) (er hard? 'top-level "Illegal inputs, ~x0 and ~x1." a b) (er soft 'top-level "Illegal inputs, ~x0 and ~x1." a b)The examples above all print an error message to standard output saying that
a and b are illegal inputs. However, the first two abort evaluation
after printing an error message, while the third returns (mv t nil state)
after printing an error message. The result in the third case can be
interpreted as 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.
Er is a macro, and the above three examples expand to calls of ACL2
functions, as shown below. See illegal, see hard-error, and see error1,
respectively.
General forms:
(er hard ctx fmt-string arg1 arg2 ... argk)
==> {macroexpands, in essence, to:}
(ILLEGAL CTX FMT-STRING
(LIST (CONS #\0 ARG1) (CONS #\1 ARG2) ... (CONS #\k ARGk)))
(er hard? ctx fmt-string arg1 arg2 ... argk)
==> {macroexpands, in essence, to:}
(HARD-ERROR CTX FMT-STRING
(LIST (CONS #\0 ARG1) (CONS #\1 ARG2) ... (CONS #\k ARGk)))
(er soft ctx fmt-string arg1 arg2 ... argk)
==> {macroexpands, in essence, to:}
(ERROR1 CTX FMT-STRING
(LIST (CONS #\0 ARG1) (CONS #\1 ARG2) ... (CONS #\k ARGk)))
