built-in ACL2 functions
Major Section:  PROGRAMMING

This documentation topic is a parent topic under which we include documentation for built-in functions, macros, and special forms that are typically used in programming. For others, including those typically used as top-level commands or those that create events (defun, defthm, and so on), documentation may be found as a subtopic of some other parent topic. We do not 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.