		Search-engine friendly clone of the ACL2 documentation.

Isodata-implementation

Isodata-input-processing

Input processing performed by isodata.

See input processing for general background.

Subtopics

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