ACL2-PC::COMMENT

(primitive) insert a comment
Major Section:  PROOF-CHECKER-COMMANDS

Example:
(comment now begin difficult final goal)

General Form: (comment &rest x)

This instruction makes no change in the state except to insert the comment instruction.

Some comments can be used to improve the display of commands; see documentation for comm.