• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Community
  • Proof-automation
  • ACL2
  • Macro-libraries
    • B*
    • Defunc
    • Fty
    • Apt
      • Simplify-defun
      • Isodata
        • Isodata-implementation
          • Isodata-event-generation
          • Isodata-fn
          • Isodata-input-processing
            • Isodata-symbol-isomap-alistp
            • Isodata-isomapp
            • Isodata-pos-isomap-alistp
            • Isodata-process-iso
            • Isodata-process-inputs
            • Isodata-process-arg/res-list-iso
            • Isodata-process-isomaps
            • Isodata-fresh-defiso-thm-names
            • Isodata-process-arg/res-list
            • Isodata-process-arg/res-list-iso-list
            • Isodata-process-res
            • Isodata-fresh-defiso-name-with-*s-suffix
            • Isodata-process-newp-of-new-name
            • 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
            • Isodata-process-undefined
            • Isodata-process-arg/res-list-aux
            • Isodata-isomap-listp
            • Isodata-fresh-defiso-name-with-*s-suffix-aux
          • Isodata-macro-definition
      • Tailrec
      • Schemalg
      • Restrict
      • Expdata
      • Casesplit
      • Simplify-term
      • Simplify-defun-sk
      • Parteval
      • Solve
      • Wrap-output
      • Propagate-iso
      • Simplify
      • Finite-difference
      • Drop-irrelevant-params
      • Copy-function
      • Lift-iso
      • Rename-params
      • Utilities
      • Simplify-term-programmatic
      • Simplify-defun-sk-programmatic
      • Simplify-defun-programmatic
      • Simplify-defun+
      • Common-options
      • Common-concepts
    • Std/util
    • Defdata
    • Defrstobj
    • Seq
    • Match-tree
    • Defrstobj
    • With-supporters
    • Def-partial-measure
    • Template-subst
    • Soft
    • Defthm-domain
    • Event-macros
    • Def-universal-equiv
    • Def-saved-obligs
    • With-supporters-after
    • Definec
    • Sig
    • Outer-local
    • Data-structures
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• 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