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 >