• 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
          • Support
          • Defthm-signed-byte-p
          • Defthm-unsigned-byte-p
          • Defthm-natp
          • Defund-sk
          • Defmacro+
          • Defsum
          • Defthm-commutative
          • Definj
          • Defirrelevant
          • Defredundant
        • Std/strings
        • Std/io
        • Std/osets
        • 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

    Defarbrec-info->expansion

    Access the expansion field of a defarbrec-infop structure.