|
|
|---|
|
|
|
|---|
A name created by a logical event
Examples: assoc caddr + "ACL2-USER" "arith" "project/task-1/arith.lisp" :here
A logical name is either a name introduced by some event, such as defun, defthm, or include-book, or else is the keyword
The logical name introduced by an include-book is the full book name
string for the book (see full-book-name). Thus, under the appropriate
setting for the current book directory (see cbd) the event
"/usr/home/smith/project/task-1/arith.lisp" .
Under a different cbd setting, it may introduce a different logical name, perhaps
"/local/src/acl2/library/arith.lisp" .
It is possible that identical include-book events forms in a session introduce two different logical names because of the current book directory.
A logical name that is a string is either a package name or a book name.
If it is not a package name, we support various conventions to interpret it as
a book name. If it does not end with the string
Logical names are used primarily in the theory manipulation functions, e.g., universal-theory and current-theory with which you may obtain some standard theories as of some point in the historical past. The reference points are the introductions of logical names, i.e., the past is determined by the events it contains. One might ask, ``Why not discuss the past with the much more flexible language of command descriptors?'' (See command-descriptor.) The reason is that inside of such events as encapsulate or macro commands that expand to progns of events, command descriptors provide too coarse a grain.
When logical names are used as referents in theory expressions used in books, one must consider the possibility that the defining event within the book in question becomes redundant by the definition of the name prior to the assumption of the book. See redundant-events.