TTAG NOTE printing
Major Section: SWITCHES-PARAMETERS-AND-MODES
General Form: (set-deferred-ttag-notes val state)where
val is t or nil.
See defttag for a discussion of trust tags (ttags). By default, a
``TTAG NOTE'' is printed in order to indicate reliance on a ttag. When
many such notes are printed, it may be desirable to avoid seeing them all.
Upon evaluation of the form
(set-deferred-ttag-notes t state)ACL2 will enter a deferred mode for the printing of ttag notes. In this mode, only the first ttag note is printed for each top-level command, and the remainder are summarized before the next top-level prompt (if any) is printed, hence before the next command is evaluated. That summary is merely a list of ttags, but the summary explains that the full ttag notes may be printed with the command
(show-ttag-notes).Note that (show-ttag-notes) spares you duplicate ttag notes. If you want
to see every ttag note as it would normally appear, for maximum security, do
not evaluate the command (set-deferred-ttag-notes t state). You can undo
the effect of this command, returning to an immediate mode for printing ttag
notes, by evaluating:
(set-deferred-ttag-notes nil state)
