Major Section: MISCELLANEOUS
ACL2 functions, e.g., if, that show enter-boot-strap-mode as their
defining command are in fact primitives. It is impossible for the
system to display defining axioms about these symbols.
Enter-boot-strap-mode is a Common Lisp function but not an ACL2
function. It magically creates from nil an ACL2 property list world
that lets us start the boot-strapping process. That is, once
enter-boot-strap-mode has created its world, it is possible to
process the defconsts, defuns, and defaxioms, necessary to bring up
the rest of the system. Before that world is created, the attempt
by ACL2 even to translate a defun form, say, would produce an error
because defun is undefined.
Several ACL2 functions show enter-boot-strap-mode as their defining
command. Among them are if, cons, car, and cdr. These functions
are characterized by axioms rather than definitional equations --
axioms that in most cases are built into our code and hence do not
have any explicit representation among the rules and formulas in the
system.
