• 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
      • Defines
      • Define-sk
      • 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
  • Community
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Defarbrec-infop

Defarbrec-info->call$

Access the call$ field of a defarbrec-infop structure.