		Search-engine friendly clone of the ACL2 documentation.

Expdata-implementation

Expdata-input-processing

Input processing performed by expdata.

See input processing for general background.

Subtopics

Expdata-symbol-surjmap-alistp: Recognize alists from symbols to surjective mapping records.
Expdata-surjmapp: Information about a surjective mapping according to which (some of) the target function's arguments and results are transformed.
Expdata-pos-surjmap-alistp: Recognize alists from positive integers to surjective mapping records.
Expdata-process-surj: Process a surj component of the surjmaps input.
Expdata-process-arg/res-list-surj: Process an (arg/res-list surj) component of the surjmaps input.
Expdata-process-inputs: Process all the inputs.
Expdata-process-surjmaps: Process the surjmaps input.
Expdata-fresh-defsurj-thm-names: Return fresh defsurj theorem names.
Expdata-process-arg/res-list: Process an arg/res-list component of the surjmaps input.
Expdata-process-arg/res-list-surj-list: Lift expdata-process-arg/res-list-surj to lists.
Expdata-process-res: Process a result specification in the surjmap input.
Expdata-process-newp-of-new-name: Process the :newp-of-new-name input.
Expdata-fresh-defsurj-name-with-*s-suffix: Suffix a name with as many *s as needed to make it a valid name for a new defsurj.
Expdata-process-surjmaps-ress
Expdata-process-surjmaps-args
Expdata-process-arg/res-list-surj-add-args
Expdata-process-arg/res-list-surj-add-ress
Expdata-process-old: Process the old input.
Expdata-process-arg/res-list-aux
Expdata-surjmap-listp: Recognize lists of surjective mapping records.
Expdata-fresh-defsurj-name-with-*s-suffix-aux