built-in ACL2 functions
Major Section:  ACL2 Documentation

The built-in ACL2 functions that one typically uses in writing programs are listed below. See their individual documentations. We do not bother to document some of the more obscure functions provided by ACL2 that do not correspond to functions of Common Lisp.

Some Related Topics

See any documentation for Common Lisp for more details on many of these functions.