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 the some of the more obscure functions provided by ACL2 that do not correspond to functions of Common Lisp.

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