		Search-engine friendly clone of the ACL2 documentation.

Support

Look-up-guard

(look-up-guard fn world) looks up the guard of the function fn, or causes a hard error if fn isn't a function.

Definitions and Theorems

Function: look-up-guard

(defun look-up-guard (fn world)
  (declare (xargs :guard (and (symbolp fn)
                              (plist-worldp world))))
  (b* ((?tmp (look-up-formals fn world)))
    (getprop fn 'guard
             t 'acl2::current-acl2-world
             world)))