Major Section: PROOF-CHECKER-COMMANDS
Example: (illegal -3)Probably not of interest to most users; always ``fails'' since it expands to the
General Form: (illegal instruction)
illegal command is used mainly in the implementation. For
example, the instruction
0 is ``read'' as
(illegal 0), since
expects positive integers.