/usr/share/acl2-4.3/books/tools/progndollar.lisp is in acl2-books-source 4.3-3.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 | (in-package "ACL2")
;; Evaluates several expressions, returning the value of the last one.
;; For example:
#||
ACL2 !>(progn$ (cons 'a 'b) (cw "Hello~%") (list 1 2 3))
Hello
(1 2 3)
||#
(defmacro progn$ (&rest rst)
(cond ((null rst) nil)
((null (cdr rst)) (car rst))
(t (xxxjoin 'prog2$ rst))))
|