		Search-engine friendly clone of the ACL2 documentation.

Std/system/function-queries

Ubody+

Enhanced variant of ubody.

Signature
(ubody+ fn wrld) → body
Arguments: fn — Guard (pseudo-termfnp fn).; wrld — Guard (plist-worldp wrld).
Returns: body — Type (pseudo-termp body).

This returns the same result as ubody, but it includes a run-time check (which should always succeed) on the result that allows us to prove the return type theorem without strengthening the guard on wrld. Furthermore, this utility causes an error if called on a symbol that does not name a function.

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__))
  (if
   (and (symbolp fn)
        (not (function-symbolp fn wrld)))
   (raise "The symbol ~x0 does not name a function."
          fn)
   (b*
    ((result (ubody fn wrld)))
    (if
     (pseudo-termp result)
     result
     (raise
      "Internal error: ~
                the unnormalized body ~x0 of ~x1 is not a pseudo-term."
      result fn))))))

Theorem: pseudo-termp-of-ubody+

(defthm pseudo-termp-of-ubody+
        (b* ((body (ubody+ fn wrld)))
            (pseudo-termp body))
        :rule-classes :rewrite)