• 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

    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))