Major Section: PROGRAMMING See hard-error, see illegal, and see
cw for examples of functions to call in the first argument of
(Prog2$ x y) equals y; the value of x is ignored. x is first
evaluated for side effect. Since the ACL2 programming language
is applicative, there can be no logical impact x may involve a
call of a function such illegal, which can cause so-called
``hard errors'', or a call of cw to perform output. Here is a
simple, contrived example using hard-error. The intention is to
check at run-time that the input is appropriate before calling
(defun foo-a (x) (declare (xargs :guard (consp x))) (prog2$ (or
(good-car-p (car x)) (hard-error 'foo-a "Bad value for x: ~p0"
(list (cons #\0 x)))) (bar x)))The following similar function
uses illegalhas a guard of nil, guard verification would
guarantee that the call of illegalbelow will never be made (at
least when guard checking is on; see set-guard-checking). (defun
foo-b (x) (declare (xargs :guard (and (consp x) (good-car-p (car
x))))) (prog2$ (or (good