• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • ACL2
    • Macro-libraries
      • B*
      • Defunc
      • Fty
      • 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
        • 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
    • 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))