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.

The difference between the hard and hard? forms is one of guards. Use hard if you want the call to generate a (clearly impossible) guard proof obligation of (essentially) NIL. But use hard? if you want to be able to call this function in guard-verified code, since the call generates a (trivially satisfied) guard proof obligation of T.

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. The first two have guards of (essentially) NIL and T, respectively, while error1 is in :program mode.

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)))