Names of all the theorems in a scope of a variable table.
(atc-symbol-varinfo-alist-to-thms scope) → thms
Function:
(defun atc-symbol-varinfo-alist-to-thms (scope) (declare (xargs :guard (atc-symbol-varinfo-alistp scope))) (let ((__function__ 'atc-symbol-varinfo-alist-to-thms)) (declare (ignorable __function__)) (b* (((when (endp scope)) nil) ((cons & info) (car scope)) (thm (atc-var-info->thm info)) (more-thms (atc-symbol-varinfo-alist-to-thms (cdr scope)))) (cons thm more-thms))))
Theorem:
(defthm symbol-listp-of-atc-symbol-varinfo-alist-to-thms (b* ((thms (atc-symbol-varinfo-alist-to-thms scope))) (symbol-listp thms)) :rule-classes :rewrite)