A table to control indentation for pretty-printing
ACL2 output is generally pretty-printed: that is, spacing and
indentation are controlled to enhance readability and aesthetics of the
output. Indentation may be controlled by using the table,
The initial value of the
(defconst *ppr-special-syms* '((case . 1) (case-match . 1) (defabsstobj . 1) (defaxiom . 1) (defchoose . 3) (defcong . 2) (defconst . 1) (defmacro . 2) (defstobj . 1) (defthm . 1) (defthmd . 1) (defun . 2) (defun-inline . 2) (defun-sk . 2) (defund . 2) (encapsulate . 1) (if . 2) (lambda . 1) (lambda$ . 1) (let . 1) (let* . 1) (mutual-recursion . 0) (mv-let . 2) (table . 1)))
For calls of special forms and macros in the
(LET ((A B) (C D)) (F A C))
Since `if' has a special-term-num of 2, the first two arguments are printed normally and the other is indented by 2, for example as follows.
Macros often have as their first argument a symbol, so these are treated
specially by putting them on the first line and any remaining arguments before
the body arguments begin on the same line if there is space. For example,
(DEFUN FOO (X Y Z) (F X Y Z))
Keyword pairs in macro calls can occur in other places than at the end of an argument list, so keyword pairing is done more aggressively, as in the following output.
(DEFINE FOO ((X P1) (Y P2)) :GUARD (P3 X Y) (F X Y Z))