Major Section: EVENTS
Examples: (local (defthm hack1 (implies (and (acl2-numberp x) (acl2-numberp y) (equal (* x y) 1)) (equal y (/ x))))) (local (defun double-naturals-induction (a b) (cond ((and (integerp a) (integerp b) (< 0 a) (< 0 b)) (double-naturals-induction (1- a) (1- b))) (t (list a b))))) General Form: (local ev)where
evis an event form. If the current default defun-mode (see default-defun-mode) is
(local ev)is equivalent to
ev. But if the current default defun-mode is
(local ev)is a
no-op. Thus, if such forms are in the event list of an
encapsulateevent or in a book, they are processed when the encapsulation or book is checked for admissibility in
logicmode but are skipped when extending the host world. Such events are thus considered ``local'' to the verification of the encapsulation or book. The non-local events are the ones ``exported'' by the encapsulation or book. See encapsulate for a thorough discussion. Also see local-incompatibility for a discussion of a commonly encountered problem with such event hiding: you can't make an event local if its presence is required to make sense of a non-local one.
Note that events that change the default defun-mode, and in fact any
events that set the
acl2-defaults-table, are disallowed inside
the scope of
local. See embedded-event-form.