• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
      • Apt
        • Simplify-defun
        • Isodata
        • Tailrec
        • Schemalg
        • Restrict
        • Expdata
          • Expdata-implementation
            • Expdata-event-generation
            • Expdata-fn
            • Expdata-input-processing
              • Expdata-symbol-surjmap-alistp
              • Expdata-surjmapp
                • Expdata-surjmap
                • Make-expdata-surjmap
                  • Change-expdata-surjmap
                  • Honsed-expdata-surjmap
                  • Make-honsed-expdata-surjmap
                  • Expdata-surjmap->surjname
                  • Expdata-surjmap->oldp-guard
                  • Expdata-surjmap->oldp
                  • Expdata-surjmap->newp-guard
                  • Expdata-surjmap->newp
                  • Expdata-surjmap->localp
                  • Expdata-surjmap->hints
                  • Expdata-surjmap->forth-injective
                  • Expdata-surjmap->forth-image
                  • Expdata-surjmap->forth-guard
                  • Expdata-surjmap->forth
                  • Expdata-surjmap->back-of-forth
                  • Expdata-surjmap->back-image
                  • Expdata-surjmap->back-guard
                  • Expdata-surjmap->back
                • Expdata-pos-surjmap-alistp
                • Expdata-process-surj
                • Expdata-process-arg/res-list-surj
                • Expdata-process-inputs
                • Expdata-process-surjmaps
                • Expdata-fresh-defsurj-thm-names
                • Expdata-process-arg/res-list
                • Expdata-process-arg/res-list-surj-list
                • Expdata-process-res
                • Expdata-process-newp-of-new-name
                • Expdata-fresh-defsurj-name-with-*s-suffix
                • Expdata-process-surjmaps-ress
                • Expdata-process-surjmaps-args
                • Expdata-process-arg/res-list-surj-add-args
                • Expdata-process-arg/res-list-surj-add-ress
                • Expdata-process-old
                • Expdata-process-arg/res-list-aux
                • Expdata-surjmap-listp
                • Expdata-fresh-defsurj-name-with-*s-suffix-aux
              • Expdata-macro-definition
          • 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
        • Pfcs
        • Wp-gen
        • Dimacs-reader
        • Legacy-defrstobj
        • Proof-checker-array
        • Soft
        • C
        • Farray
        • Rp-rewriter
        • Instant-runoff-voting
        • Imp-language
        • Sidekick
        • Leftist-trees
        • Java
        • Taspi
        • Riscv
        • Bitcoin
        • 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
        • Aleo
        • Bigmems
        • Builtins
        • Execloader
        • Solidity
        • Paco
        • Concurrent-programs
        • Bls12-377-curves
      • Debugging
      • Std
      • Community
      • Proof-automation
      • ACL2
      • Macro-libraries
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Expdata-surjmapp

    Make-expdata-surjmap

    Constructor macro for expdata-surjmapp structures.

    Syntax:

    (make-expdata-surjmap [:surjname <surjname>] 
                          [: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-injective <forth-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 expdata-surjmapp structures. It simply conses together a structure with the specified fields.

    This macro generates a new expdata-surjmapp structure from scratch. See also change-expdata-surjmap, which can "change" an existing structure, instead.

    The expdata-surjmapp structures we create here are just constructed with ordinary cons. If you want to create honsed structures, see make-honsed-expdata-surjmap instead.

    Definition

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

    Macro: make-expdata-surjmap

    (defmacro make-expdata-surjmap (&rest args)
      (std::make-aggregate 'expdata-surjmap
                           args
                           '((:surjname)
                             (:localp)
                             (:oldp)
                             (:newp)
                             (:forth)
                             (:back)
                             (:forth-image)
                             (:back-image)
                             (:back-of-forth)
                             (:forth-injective)
                             (:oldp-guard)
                             (:newp-guard)
                             (:forth-guard)
                             (:back-guard)
                             (:hints))
                           'make-expdata-surjmap
                           nil))