Project the recognizers out of an external object information alist.
(atc-string-objinfo-alist-to-recognizers prec-objs) → recognizers
Function:
(defun atc-string-objinfo-alist-to-recognizers (prec-objs) (declare (xargs :guard (atc-string-objinfo-alistp prec-objs))) (let ((__function__ 'atc-string-objinfo-alist-to-recognizers)) (declare (ignorable __function__)) (b* (((when (endp prec-objs)) nil) (info (cdar prec-objs)) (recognizer (defobject-info->recognizer (atc-obj-info->defobject info))) (more-recognizers (atc-string-objinfo-alist-to-recognizers (cdr prec-objs)))) (cons recognizer more-recognizers))))
Theorem:
(defthm symbol-listp-of-atc-string-objinfo-alist-to-recognizers (b* ((recognizers (atc-string-objinfo-alist-to-recognizers prec-objs))) (symbol-listp recognizers)) :rule-classes :rewrite)