		Search-engine friendly clone of the ACL2 documentation.

Std/system/function-queries

Unwrapped-nonexec-body

Body of a non-executable defined named function, without the ``non-executable wrapper''.

Signature
(unwrapped-nonexec-body fn wrld) → unwrapped-body
Arguments: fn — Guard (symbolp fn).; wrld — Guard (plist-worldp wrld).
Returns: unwrapped-body — A pseudo-termp.

defun-nx generates a logic-mode function whose body is wrapped as follows:

(return-last 'progn
             (throw-nonexec-error 'fn
                                  (cons arg1 ... (cons argN 'nil)...))
             body)

If defun is used for a logic-mode function with :non-executable set to t, the submitted body (once translated) must be wrapped as above.

It is also possible to use defun to introduce program-mode functions with :non-executable set to :program, in which case the body must be wrapped as above. (These defuns are introduced via defproxy.)

This utility returns the unwrapped body of a logic-mode or program-mode defined non-executable function fn, by removing the wrapper shown above. Here, `defined' means that the function has an unnormalized-body property, which is retrieved and unwrapped.

See unwrapped-nonexec-body+ for an enhanced variant of this utility.

Definitions and Theorems

Function: unwrapped-nonexec-body

(defun unwrapped-nonexec-body (fn wrld)
  (declare (xargs :guard (and (symbolp fn) (plist-worldp wrld))))
  (let ((__function__ 'unwrapped-nonexec-body))
    (declare (ignorable __function__))
    (fourth (ubody fn wrld))))