Retrieve the information about a tag from a tag table.
(atc-get-tag-info tag prec-tags) → info
This is always called on tag that are in the table, so we thrown an internal error if the tag is not in the table.
Function:
(defun atc-get-tag-info (tag prec-tags) (declare (xargs :guard (and (identp tag) (atc-string-taginfo-alistp prec-tags)))) (let ((__function__ 'atc-get-tag-info)) (declare (ignorable __function__)) (b* ((info (cdr (assoc-equal (ident->name tag) prec-tags))) ((unless (atc-tag-infop info)) (raise "Internal error: no information for tag ~x0." tag) (irr-atc-tag-info))) info)))
Theorem:
(defthm atc-tag-infop-of-atc-get-tag-info (b* ((info (atc-get-tag-info tag prec-tags))) (atc-tag-infop info)) :rule-classes :rewrite)