• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
      • Std/lists
      • Std/alists
      • Obags
      • Std/util
        • Defprojection
        • Deflist
        • Defaggregate
        • Define
          • Returns-specifiers
          • Extended-formals
          • Defret
            • Defretgen
              • Defretgen-rules
              • Defret-mutual-generate
              • Def-retgen-fnset
            • Define-guards
            • Defret-mutual
            • Post-define-hook
            • More-returns
            • Raise
          • Defmapping
          • Defenum
          • Add-io-pairs
          • Defalist
          • Defmapappend
          • Returns-specifiers
          • Defarbrec
          • 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
    • Defretgen

    Def-retgen-fnset

    Give a name to a set of functions and mutual recursions that may be used in defretgen.

    Usage:

    (defretgen my-function-set
       (a-name
        (:fnset a-fnset-name)
        (:function a-function-name)
        (:mutrec a-mutrec-name)))

    The first argument to defretgen is the new name for the set; the second argument is the set of functions, mutual recursions, and preexisting sets that are included in the new set.