List of the formals of a function that represent external objects.
(atc-typed-formals-to-extobjs typed-formals) → extobjs
Function:
(defun atc-typed-formals-to-extobjs (typed-formals) (declare (xargs :guard (atc-symbol-varinfo-alistp typed-formals))) (let ((__function__ 'atc-typed-formals-to-extobjs)) (declare (ignorable __function__)) (b* (((when (endp typed-formals)) nil) ((cons formal info) (car typed-formals))) (if (atc-var-info->externalp info) (cons formal (atc-typed-formals-to-extobjs (cdr typed-formals))) (atc-typed-formals-to-extobjs (cdr typed-formals))))))
Theorem:
(defthm symbol-listp-of-atc-typed-formals-to-extobjs (implies (atc-symbol-varinfo-alistp typed-formals) (b* ((extobjs (atc-typed-formals-to-extobjs typed-formals))) (symbol-listp extobjs))) :rule-classes :rewrite)