SET-BRR-TERM-EVISC-TUPLE

controls printing of terms inside the break-rewrite loop
Major Section:  BREAK-REWRITE

This macro controls printing of terms inside the break-rewrite loop (see break-rewrite).

Examples:
(set-brr-term-evisc-tuple nil) ; default (inside brr)
(set-brr-term-evisc-tuple '(nil 3 4 nil))
The first of the examples above restores the break-rewrite state to one in which terms are printed in full. The second sets the print-level to 3 and the print-length to 4, to replace substructures deeper than 3 by ``#'' and those longer than 4 by ``...''; see see ld-evisc-tuple for information about the shape of the argument of this macro, which is evaluated.

This macro can be executed either inside a break from break-rewrite, or at the top level. Its effect will persist, except potentially when you execute ``#.'' to exit break-rewrite.

Here is an example showing the effect of this macro.

1 ACL2 >:unify-subst
     X : (CONS A
               (CONS B
                     (CONS C
                           (CONS D (CONS E (CONS F (CONS G 'NIL)))))))
1 ACL2 >(set-brr-term-evisc-tuple (evisc-tuple 3 4 nil nil))
<state>
1 ACL2 >:unify-subst
     X : (CONS A (CONS B (CONS C #)))
1 ACL2 >