cws - ACL2 Book

other

(in-package "ACL2")

cwvalmacro

(defmacro cwval
  (expr)
  `(let ((cw-val ,EXPR))
    (prog2$ (cw "~x0: ~x1~%" ',EXPR cw-val) cw-val)))

cws-fnfunction

(defun cws-fn
  (lst)
  (if (atom lst)
    nil
    (cons `(cwval ,(CAR LST)) (cws-fn (cdr lst)))))

cwsmacro

(defmacro cws (&rest lst) (cons 'progn$ (cws-fn lst)))