SYNTAX

the syntax of ACL2 is that of Common Lisp
Major Section:  MISCELLANEOUS

For the details of ACL2 syntax, see CLTL. For examples of ACL2 syntax, use :pe to print some of the ACL2 system code. For example:

:pe assoc-equal
:pe dumb-occur
:pe var-fn-count
:pe add-linear-variable-to-alist

There is no comprehensive description of the ACL2 syntax yet, except that found in CLTL. Also see term.