		Search-engine friendly clone of the ACL2 documentation.

Std/system/function-queries

Formals+

Enhanced variant of formals.

Signature
(formals+ fn wrld) → formals
Arguments: fn — Guard (pseudo-termfnp fn).; wrld — Guard (plist-worldp wrld).
Returns: formals — Type (symbol-listp formals).

This returns the same result as formals on named functions, 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.

Similarly to formals, this utility causes an error if called on a symbol that does not name a function. But the error message is slightly different from the one of formals.

This utility also operates on lambda expressions, unlike formals.

Definitions and Theorems

Function: formals+

(defun
 formals+ (fn wrld)
 (declare (xargs :guard (and (pseudo-termfnp fn)
                             (plist-worldp wrld))))
 (let
  ((__function__ 'formals+))
  (declare (ignorable __function__))
  (b*
   ((result
       (if (symbolp fn)
           (b* ((formals (getpropc fn 'formals t wrld)))
               (if (eq formals t)
                   (raise "The symbol ~x0 does not name a function."
                          fn)
                   formals))
           (lambda-formals fn))))
   (if
    (symbol-listp result)
    result
    (raise
     "Internal error: ~
              the formals ~x0 of ~x1 are not a true list of symbols."
     result fn)))))

Theorem: symbol-listp-of-formals+

(defthm symbol-listp-of-formals+
        (b* ((formals (formals+ fn wrld)))
            (symbol-listp formals))
        :rule-classes :rewrite)