Enhanced variant of 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
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)