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. 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.