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