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 ev is an event form. If the current default defun-mode
(see default-defun-mode) is :logic and ld-skip-proofsp is
nil or t, then (local ev) is equivalent to ev. But if
the current default defun-mode is :program or if
ld-skip-proofsp is 'include-book, then (local ev) is a
no-op. Thus, if such forms are in the event list of an
encapsulate event or in a book, they are processed when the
encapsulation or book is checked for admissibility in :logic mode
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.
