Ubody
Unnormalized body of a named function,
or body of a lambda expression.
- Signature
(ubody fn wrld) → body
- Arguments
- fn — Guard (pseudo-termfnp fn).
- wrld — Guard (plist-worldp wrld).
- Returns
- body — A pseudo-termp.
This is a specialization of the built-in body
with nil as the second argument.
Since body is not guard-verified only because of
the code that handles the case
in which the second argument is non-nil,
we avoid calling body and instead replicate
the (simple) code that handles the case
in which the second argument is nil;
thus, this utility is guard-verified.
The unnormalized body of a named function
is its unnormalized-body property.
If a function is not defined, this property is nil.
Some program-mode functions may be defined
but not have an unnormalized-body property.
If a function does not have an unnormalized-body property,
this utility returns nil.
See ubody+ for an enhanced variant of this utility.
Definitions and Theorems
Function: ubody
(defun ubody (fn wrld)
(declare (xargs :guard (and (pseudo-termfnp fn)
(plist-worldp wrld))))
(let ((__function__ 'ubody))
(declare (ignorable __function__))
(cond ((symbolp fn)
(getpropc fn 'unnormalized-body
nil wrld))
(t (lambda-body fn)))))
