		Search-engine friendly clone of the ACL2 documentation.

Parteval-input-processing

Input processing performed by parteval.

See input processing for general background.

Parteval-process-inputs: Process all the inputs.
Parteval-unchanging-static-in-rec-calls-p: Check if the static parameters do not change in the arguments of the recursive calls of old.
Parteval-process-static-terms: Process the c1, ..., cm parts of the static input.
Parteval-unchanging-static-in-rec-args-p: Check if the static parameters do not change in the arguments of a recursive call of old.
Parteval-process-thm-name: Process the :thm-name input.
Parteval-process-static: Process the static input.
Parteval-process-old: Process the old input.
Parteval-case-of-old: Classify old into one of the three cases described in the reference documentation.