• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
      • Std/lists
      • Std/alists
      • Obags
      • Std/util
        • Defprojection
        • Deflist
        • Defaggregate
        • Define
        • Defmapping
        • Defenum
        • Add-io-pairs
        • Defalist
        • Defmapappend
        • Returns-specifiers
        • Defarbrec
          • Defarbrec-implementation
            • Defarbrec-event-generation
            • Defarbrec-input-processing
            • Defarbrec-check-redundancy
            • Defarbrec-fn
            • Defarbrec-table
              • Defarbrec-infop
                • Defarbrec-info
                • Make-defarbrec-info
                  • Change-defarbrec-info
                  • Honsed-defarbrec-info
                  • Make-honsed-defarbrec-info
                  • Defarbrec-info->x1...xn
                  • Defarbrec-info->update-fns
                  • Defarbrec-info->terminates-fn
                  • Defarbrec-info->measure-fn
                  • Defarbrec-info->expansion
                  • Defarbrec-info->call$
                  • Defarbrec-info->body
                • Defarbrec-filter-call
                • *defarbrec-table-name*
              • Defarbrec-macro-definition
          • Define-sk
          • Defines
          • Error-value-tuples
          • Defmax-nat
          • Defmin-int
          • Deftutorial
          • Extended-formals
          • Defrule
          • Defval
          • Defsurj
          • Defiso
          • Defconstrained-recognizer
          • Deffixer
          • Defmvtypes
          • Defconsts
          • Defthm-unsigned-byte-p
          • Support
          • Defthm-signed-byte-p
          • Defthm-natp
          • Defund-sk
          • Defmacro+
          • Defsum
          • Defthm-commutative
          • Definj
          • Defirrelevant
          • Defredundant
        • Std/strings
        • Std/osets
        • Std/io
        • Std/basic
        • Std/system
        • Std/typed-lists
        • Std/bitsets
        • Std/testing
        • Std/typed-alists
        • Std/stobjs
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Defarbrec-infop

    Make-defarbrec-info

    Constructor macro for defarbrec-infop structures.

    Syntax:

    (make-defarbrec-info [:call$ <call$>] 
                         [:expansion <expansion>] 
                         [:x1...xn <x1...xn>] 
                         [:body <body>] 
                         [:update-fns <update-fns>] 
                         [:terminates-fn <terminates-fn>] 
                         [:measure-fn <measure-fn>]) 
    

    This is our preferred way to construct defarbrec-infop structures. It simply conses together a structure with the specified fields.

    This macro generates a new defarbrec-infop structure from scratch. See also change-defarbrec-info, which can "change" an existing structure, instead.

    The defarbrec-infop structures we create here are just constructed with ordinary cons. If you want to create honsed structures, see make-honsed-defarbrec-info instead.

    Definition

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

    Macro: make-defarbrec-info

    (defmacro make-defarbrec-info (&rest args)
      (std::make-aggregate 'defarbrec-info
                           args
                           '((:call$)
                             (:expansion)
                             (:x1...xn)
                             (:body)
                             (:update-fns)
                             (:terminates-fn)
                             (:measure-fn))
                           'make-defarbrec-info
                           nil))