Ld-evisc-tuple
Determines whether ld suppresses details when printing
Ld-evisc-tuple is an ld special (see ld). The
accessor is (ld-evisc-tuple state) and an updater is
(set-ld-evisc-tuple val state), although the use of set-evisc-tuple is preferred for updating. Ld-evisc-tuple must be
either nil, which is its initial value, or a legal evisc-tuple: see set-evisc-tuple.
The general-purpose ACL2 read-eval-print loop, ld, reads forms from
standard-oi, evaluates them and prints the result to standard-co. Note that the ACL2 top-level loop (see lp) results from
an invocation of ld.
However, there are various flags that control ld's behavior and
ld-evisc-tuple is one of them. Ld may print the forms it is
evaluating and/or the results of evaluation. Depending on the value of
ld-evisc-tuple ld may ``eviscerate'' objects before printing
them. See set-evisc-tuple for a discussion of evisceration and of how
other evisc-tuples affect the printing of error messages and warnings, as well
as other output not from ld.