The syntax of ACL2 is that of Common Lisp
For the details of ACL2 syntax, see CLTL. For examples of ACL2
syntax, use
: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.