		Search-engine friendly clone of the ACL2 documentation.

Std/system/function-queries

Uguard+

Enhanced variant of uguard.

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

This returns the same result as uguard, 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: uguard+

(defun
 uguard+ (fn wrld)
 (declare (xargs :guard (and (pseudo-termfnp fn)
                             (plist-worldp wrld))))
 (let
  ((__function__ 'uguard+))
  (declare (ignorable __function__))
  (if
   (and (symbolp fn)
        (not (function-symbolp fn wrld)))
   (raise "The symbol ~x0 does not name a function."
          fn)
   (b*
    ((result (uguard fn wrld)))
    (if
     (pseudo-termp result)
     result
     (raise
      "Internal error: ~
                the guard ~x0 of ~x1 is not a pseudo-term."
      result fn))))))

Theorem: pseudo-termp-of-uguard+

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