		Search-engine friendly clone of the ACL2 documentation.

Support

Look-up-formals

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

Definitions and Theorems

Function: look-up-formals

(defun look-up-formals (fn world)
  (declare (xargs :guard (and (symbolp fn)
                              (plist-worldp world))))
  (b* ((__function__ 'look-up-formals)
       (look (getprop fn 'acl2::formals
                      :bad 'acl2::current-acl2-world
                      world))
       ((when (eq look :bad))
        (raise "Can't look up the formals for ~x0!"
               fn))
       ((unless (symbol-listp look))
        (raise "Expected a symbol-listp, but found ~x0!"
               look)))
    look))

Theorem: symbol-listp-of-look-up-formals

(defthm symbol-listp-of-look-up-formals
  (symbol-listp (look-up-formals fn world)))