Builtins
A library about the ACL2 built-ins.
The file collect.lisp contains code
to collect the names of all the built-in ACL2 events
and to store them into named constants.
That file also defines additional named constants
that categorize functions and axioms and theorems;
these could be potentially moved to a new file
called categorize.lisp at some point.
The file document.lisp contains code
to generate XDOC topics for the built-in axioms and theorems,
organized in different ways.
This makes it easier to see the built-in axioms and theorems
than looking or searching through the source code.
The file disable.lisp contains code
that can be used to disable built-in functions and rules
(the latter are axioms or theorems that have rule classes).
This may be useful for more controlled and efficient proofs.
Subtopics
- Builtin-defaxioms/defthms
- Built-in axioms and theorems.
