• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • ACL2
      • Theories
      • Rule-classes
      • Proof-builder
      • Recursion-and-induction
      • Hons-and-memoization
      • Events
      • Parallelism
      • History
      • Programming
      • Operational-semantics
      • Real
      • Start-here
      • Debugging
      • Miscellaneous
      • Output-controls
      • Macros
        • Make-event
        • Defmacro
        • Untranslate-patterns
        • Tc
        • Trans*
        • Macro-aliases-table
        • Macro-args
        • Defabbrev
        • User-defined-functions-table
        • Trans
        • Untranslate-for-execution
        • Add-macro-fn
        • Check-vars-not-free
        • Safe-mode
        • 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-isomap
                    • Make-isodata-isomap
                      • Honsed-isodata-isomap
                      • Change-isodata-isomap
                      • Make-honsed-isodata-isomap
                      • Isodata-isomap->oldp-guard
                      • Isodata-isomap->oldp
                      • Isodata-isomap->newp-guard
                      • Isodata-isomap->newp
                      • Isodata-isomap->localp
                      • Isodata-isomap->isoname
                      • Isodata-isomap->hints
                      • Isodata-isomap->forth-of-back
                      • Isodata-isomap->forth-injective
                      • Isodata-isomap->forth-image
                      • Isodata-isomap->forth-guard
                      • Isodata-isomap->forth
                      • Isodata-isomap->back-of-forth
                      • Isodata-isomap->back-injective
                      • Isodata-isomap->back-image
                      • Isodata-isomap->back-guard
                      • Isodata-isomap->back
                    • 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
          • Trans1
          • Defmacro-untouchable
          • Set-duplicate-keys-action
          • Add-macro-alias
          • Magic-macroexpand
          • Defmacroq
          • Trans!
          • Remove-macro-fn
          • Remove-macro-alias
          • Add-binop
          • Untrans-table
          • Trans*-
          • Remove-binop
          • Tcp
          • Tca
        • Mailing-lists
        • Interfacing-tools
      • 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-isomap
                  • Make-isodata-isomap
                    • Honsed-isodata-isomap
                    • Change-isodata-isomap
                    • Make-honsed-isodata-isomap
                    • Isodata-isomap->oldp-guard
                    • Isodata-isomap->oldp
                    • Isodata-isomap->newp-guard
                    • Isodata-isomap->newp
                    • Isodata-isomap->localp
                    • Isodata-isomap->isoname
                    • Isodata-isomap->hints
                    • Isodata-isomap->forth-of-back
                    • Isodata-isomap->forth-injective
                    • Isodata-isomap->forth-image
                    • Isodata-isomap->forth-guard
                    • Isodata-isomap->forth
                    • Isodata-isomap->back-of-forth
                    • Isodata-isomap->back-injective
                    • Isodata-isomap->back-image
                    • Isodata-isomap->back-guard
                    • Isodata-isomap->back
                  • 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-isomapp

      Make-isodata-isomap

      Constructor macro for isodata-isomapp structures.

      Syntax:

      (make-isodata-isomap [:isoname <isoname>] 
                           [:localp <localp>] 
                           [:oldp <oldp>] 
                           [:newp <newp>] 
                           [:forth <forth>] 
                           [:back <back>] 
                           [:forth-image <forth-image>] 
                           [:back-image <back-image>] 
                           [:back-of-forth <back-of-forth>] 
                           [:forth-of-back <forth-of-back>] 
                           [:forth-injective <forth-injective>] 
                           [:back-injective <back-injective>] 
                           [:oldp-guard <oldp-guard>] 
                           [:newp-guard <newp-guard>] 
                           [:forth-guard <forth-guard>] 
                           [:back-guard <back-guard>] 
                           [:hints <hints>]) 
      

      This is our preferred way to construct isodata-isomapp structures. It simply conses together a structure with the specified fields.

      This macro generates a new isodata-isomapp structure from scratch. See also change-isodata-isomap, which can "change" an existing structure, instead.

      The isodata-isomapp structures we create here are just constructed with ordinary cons. If you want to create honsed structures, see make-honsed-isodata-isomap instead.

      Definition

      This is an ordinary make- macro introduced by std::defaggregate.

      Macro: make-isodata-isomap

      (defmacro make-isodata-isomap (&rest args)
        (std::make-aggregate 'isodata-isomap
                             args
                             '((:isoname)
                               (:localp)
                               (:oldp)
                               (:newp)
                               (:forth)
                               (:back)
                               (:forth-image)
                               (:back-image)
                               (:back-of-forth)
                               (:forth-of-back)
                               (:forth-injective)
                               (:back-injective)
                               (:oldp-guard)
                               (:newp-guard)
                               (:forth-guard)
                               (:back-guard)
                               (:hints))
                             'make-isodata-isomap
                             nil))