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