Body of a non-executable defined named function,
without the ``non-executable wrapper''.
(unwrapped-nonexec-body fn wrld) → unwrapped-body
- fn — Guard (symbolp fn).
- wrld — Guard (plist-worldp wrld).
- unwrapped-body — A pseudo-termp.
a logic-mode function whose body is wrapped as follows:
(cons arg1 ... (cons argN 'nil)...))
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
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))))