• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
      • Kestrel-books
        • Crypto-hdwallet
        • 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
          • Error-checking
          • Fty-extensions
          • Isar
          • Kestrel-utilities
          • Set
          • Soft
          • C
          • Bv
          • Imp-language
          • Event-macros
          • Java
          • Bitcoin
          • Ethereum
          • Yul
          • Zcash
          • ACL2-programming-language
          • Prime-fields
          • Json
          • Syntheto
          • File-io-light
          • Cryptography
          • Number-theory
          • Lists-light
          • Axe
          • Builtins
          • Solidity
          • Helpers
          • Htclient
          • Typed-lists-light
          • Arithmetic-light
        • X86isa
        • Axe
        • Execloader
      • Math
      • Testing-utilities
    • Isodata-isomapp

    Change-isodata-isomap

    A copying macro that lets you create new isodata-isomapp structures, based on existing structures.

    Syntax:

    (change-isodata-isomap x 
                           [: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 a sometimes useful alternative to make-isodata-isomap. It constructs a new isodata-isomapp structure that is a copy of x, except that you can explicitly change some particular fields. Any fields you don't mention just keep their values from x.

    Definition

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

    Macro: change-isodata-isomap

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