Project the recognizers out of a tag information alist.
(atc-string-taginfo-alist-to-recognizers prec-tags) → recognizers
Function:
(defun atc-string-taginfo-alist-to-recognizers (prec-tags) (declare (xargs :guard (atc-string-taginfo-alistp prec-tags))) (let ((__function__ 'atc-string-taginfo-alist-to-recognizers)) (declare (ignorable __function__)) (b* (((when (endp prec-tags)) nil) (info (cdar prec-tags)) (recog (defstruct-info->recognizer (atc-tag-info->defstruct info))) (recogs (atc-string-taginfo-alist-to-recognizers (cdr prec-tags)))) (cons recog recogs))))
Theorem:
(defthm symbol-listp-of-atc-string-taginfo-alist-to-recognizers (b* ((recognizers (atc-string-taginfo-alist-to-recognizers prec-tags))) (symbol-listp recognizers)) :rule-classes :rewrite)