Major Section: SWITCHES-PARAMETERS-AND-MODES
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
hence its effect is
local to the book or
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
: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-occuring 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 nilrestores normal clause printing.
The mode is stored in the defaults table, See acl2-defaults-table. Thus, the mode may be set locally in books.