		Search-engine friendly clone of the ACL2 documentation.

Output-controls

Set-let*-abstractionp

To shorten many prettyprinted clauses

Note: This is an event! It does not print the usual event summary but nevertheless changes the ACL2 logical world and is so recorded. Moreover, its effect is to set the ACL2-defaults-table, and hence its effect is local to the book or encapsulate form containing it; see ACL2-defaults-table.

When this flag is set to t, subterms that occur more than once in a clause are abstracted away with let*, generally shortening the displayed size of the clauses. This flag only affects how clauses are printed. It does not change what terms the theorem prover manipulates.

:set-let*-abstractionp t ;;; or, (set-let*-abstractionp t)

will cause the prettyprinter to do ``let* abstraction'' on clauses before they are printed. The algorithm finds the maximal multiply-occurring subterm and extracts it, binding it to some new variable and replacing its occurrences by that variable. This produces a let* form. This process is iterated until no subterm occurs more than once. This process generally takes a little time, but less time than to print large clauses. The process can greatly reduce the amount of text produced by the prover.

THIS ONLY AFFECTS HOW THE CLAUSES ARE PRINTED! The unabstracted clauses are manipulated by the theorem prover.

:set-let*-abstractionp nil

restores normal clause printing.

The mode is stored in the defaults table, See ACL2-defaults-table. Thus, the mode may be set locally in books.