Ld-always-skip-top-level-locals
Determines whether ld skips local top-level forms
Ld-always-skip-top-level-locals is an ld special (see
ld). The accessor is (ld-always-skip-top-level-locals state) and
the updater is (set-ld-always-skip-top-level-locals val state). The
value of ld-always-skip-top-level-locals must be either nil or
t. The initial value of ld-always-skip-top-level-locals is
nil.
The general-purpose ACL2 read-eval-print loop, ld, is controlled by
various flags that control its behavior, and
ld-always-skip-top-level-locals is one of them. When the value is
t, local events are skipped when they are at the top level
in the following sense: they are not evaluated in the scope of either a call
of certify-book, include-book, or encapsulate, or else
during make-event expansion.
