ER

print an error message and ``cause an error''
Major Section:  ACL2-BUILT-INS

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 logically returning nil, though in ordinary evaluation the return value is never seen); 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 unless they are building systems of some sort; see programming-with-state. If state is not available in the current context then you will probably want to use (er hard ...) or (er hard? ...) to cause an error; for example, if you are returning two values, you may write (mv (er hard ...) nil).

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