		Search-engine friendly clone of the ACL2 documentation.

Events

Local

Hiding an event in an encapsulation or book

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.