Execute two forms and return the value of the second one
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: ~x0" (list (cons #\0 x)))) (bar x)))
The following similar function uses illegal instead of
(defun foo-b (x) (declare (xargs :guard (and (consp x) (good-car-p (car x))))) (prog2$ (or (good-car-p (car x)) (illegal 'foo-b "Bad value for x: ~x0" (list (cons #\0 x)))) (bar x)))
We conclude with a simple example using cw from the ACL2 sources.
(defun print-terms (terms iff-flg wrld evisc-tuple) ; Print untranslations of the given terms with respect to iff-flg, following ; each with a newline. ; We use cw instead of the fmt functions because we want to be able to use this ; function in print-type-alist-segments (used in brkpt1), which does not return ; state. (if (endp terms) terms (prog2$ (cw "~Y01" (untranslate (car terms) iff-flg wrld) evisc-tuple) (print-terms (cdr terms) iff-flg wrld evisc-tuple))))