• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
      • Theories
      • Rule-classes
        • Type-prescription
        • Rewrite
        • Meta
        • Linear
        • Definition
          • Force
          • Syntaxp
          • Bind-free
          • Case-split
          • Simple
          • Set-body
            • Show-bodies
          • Clause-processor
          • Tau-system
          • Forward-chaining
          • Equivalence
          • Free-variables
          • Congruence
          • Executable-counterpart
          • Induction
          • Compound-recognizer
          • Elim
          • Well-founded-relation-rule
          • Rewrite-quoted-constant
          • Built-in-clause
          • Well-formedness-guarantee
          • Patterned-congruence
          • Rule-classes-introduction
          • Guard-holders
          • Refinement
          • Type-set-inverter
          • Generalize
          • Corollary
          • Induction-heuristics
          • Backchaining
          • Default-backchain-limit
        • Proof-builder
        • Hons-and-memoization
        • Events
        • History
        • Parallelism
        • Programming
        • Start-here
        • Real
        • Debugging
        • Miscellaneous
        • Output-controls
        • Macros
        • Interfacing-tools
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Testing-utilities
      • Math
    • Definition
    • Events

    Set-body

    Set the definition body

    Examples:
    (set-body foo (:definition foo)) ; restore original definition of foo
    (set-body foo foo) ; same as just above
    (set-body foo my-foo-def) ; use my-foo-def for the body of foo
    (set-body foo (:definition my-foo-def)) ; same as just above

    Rules of class :definition can install a new definition body, used for example by :expand hints. See definition and also see hints for a detailed discussion of the :install-body fields of :definition rules and their role in :expand hints.

    There may be several such definitions, but by default, the latest one is used by :expand hints. Although the :with keyword may be used in :expand hints to override this behavior locally (see hints), it may be convenient to install a definition for expansion other than the latest one — for example, the original definition. Set-body may be used for this purpose.

    General Form:
    (set-body function-symbol rule-name)

    where rule-name is either a :definition rune or is a function symbol, sym, which represents the rune (:definition sym).

    You can view all definitions available for expansion; see show-bodies.