• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • 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
        • Zfc
        • Acre
        • Milawa
        • Smtlink
        • Abnf
        • Vwsim
        • Isar
        • Wp-gen
        • Dimacs-reader
        • Pfcs
        • Legacy-defrstobj
        • Proof-checker-array
        • Soft
        • C
        • Farray
        • Rp-rewriter
        • Instant-runoff-voting
        • Imp-language
        • Sidekick
        • Leftist-trees
        • Java
        • Taspi
        • Bitcoin
        • Riscv
        • Des
        • Ethereum
        • X86isa
        • Sha-2
        • Yul
        • Zcash
        • Proof-checker-itp13
        • Regex
        • ACL2-programming-language
        • Json
        • Jfkr
        • Equational
        • Cryptography
        • Poseidon
        • Where-do-i-place-my-book
        • Axe
        • Bigmems
        • Builtins
        • Execloader
        • Aleo
        • Solidity
        • Paco
        • Concurrent-programs
        • Bls12-377-curves
      • Debugging
      • Std
      • Proof-automation
      • Macro-libraries
      • ACL2
      • 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))