ER

print an error message and ``cause an error''
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)))