Restrictions on the forms inside books
Example Book: ; This book defines my app function and the theorem that it is ; associative. One irrelevant help lemma is proved first but ; it is local and so not seen by include-book. I depend on the ; inferior book "weird-list-primitives" from which I get ; definitions of hd and tl. (in-package "MY-PKG") (include-book "weird-list-primitives") (defun app (x y) (if (consp x) (cons (hd x) (app (tl x) y)) y)) (local (defthm help-lemma (implies (true-listp x) (equal (app x nil) x)))) (defthm app-is-associative (equal (app (app a b) c) (app a (app b c))))
The first form in a book must be
Because in-package is not an embedded event form, the only in-package in a book is the initial one. Because defpkg is not an embedded event form, a book can never contain a defpkg form. Because include-book is an embedded event form, books may contain references to other books. This makes books structured objects.
When the forms in a book are read from the file, they are read with current-package set to the package named in the in-package form at
the top of the file. The effect of this is that all symbols are interned in that package, except those whose packages are given explicitly
with the ``::'' notation. For example, if a book begins with
(defun fn (x) (acl2::list 'car x))
(acl2-x::defun acl2-x::fn (acl2-x::x) (acl2::list 'acl2-x::car acl2-x::x)).
If each book has its own unique package name and all the names defined
within the book are in that package, then name clashes between books
are completely avoided. This permits the construction of useful logical worlds by the successive inclusion of many books. Although it is
often too much trouble to manage several packages, their judicious use is a
way to minimize name clashes. Often, a better way is to use
How does include-book know the definitions of the packages used in a book, since defpkgs cannot be among the forms? More generally, how do we know that the forms in a book will be admissible in the host logical world of an include-book? See certificate for answers to these questions.