		Search-engine friendly clone of the ACL2 documentation.

Atc-object-tables

Atc-string-objinfo-alist-to-recognizers

Project the recognizers out of an external object information alist.

Signature
(atc-string-objinfo-alist-to-recognizers prec-objs) → recognizers
Arguments: prec-objs — Guard (atc-string-objinfo-alistp prec-objs).
Returns: recognizers — Type (symbol-listp recognizers).

Definitions and Theorems

Function: atc-string-objinfo-alist-to-recognizers

(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: symbol-listp-of-atc-string-objinfo-alist-to-recognizers

(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)