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.