Enhanced variant of formals.
(formals+ fn wrld) → 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
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.
(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)))))
(defthm symbol-listp-of-formals+ (b* ((formals (formals+ fn wrld))) (symbol-listp formals)) :rule-classes :rewrite)