		Search-engine friendly clone of the ACL2 documentation.

Support

Look-up-wrapper-args

(look-up-wrapper-args wrapper world) is like look-up-formals, except that wrapper can be either a function or a macro, and in the macro case the arguments we return may include lambda-list keywords; see macro-args.

Definitions and Theorems

Function: look-up-wrapper-args

(defun look-up-wrapper-args (wrapper world)
  (declare (xargs :guard (and (symbolp wrapper)
                              (plist-worldp world))))
  (b* ((__function__ 'look-up-wrapper-args)
       (look (getprop wrapper 'acl2::formals
                      :bad 'acl2::current-acl2-world
                      world))
       ((unless (eq look :bad)) look)
       (look (getprop wrapper 'macro-args
                      :bad 'acl2::current-acl2-world
                      world))
       ((unless (eq look :bad)) look))
    (raise "Failed to find formals or macro-args for ~x0!"
           wrapper)))