		Search-engine friendly clone of the ACL2 documentation.

Defarbrec-input-processing

Input processing performed by defarbrec.

This involves validating the inputs. When validation fails, soft errors occur. Thus, generally the input processing functions return error triples.

Defarbrec-process-terminates-name: Process the :terminates-name input.
Defarbrec-process-body: Process the body input.
Defarbrec-process-inputs: Process all the inputs.
Defarbrec-process-update-names: Process the :update-names input.
Defarbrec-process-measure-name: Process the :measure-name input.
Defarbrec-default-update-names: Default names of the iterated argument update functions.
Defarbrec-process-nonterminating: Process the :nonterminating input.
Defarbrec-process-x1...xn: Process the (x1 ... xn) input.
Defarbrec-process-print: Process the :print input.
Defarbrec-process-fn: Process the fn input.
Defarbrec-process-show-only: Process the :show-only input.
Defarbrec-printp: Recognize the allowed values of the :print input.