Enter-boot-strap-mode
The first millisecond of the Big Bang
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.
