		Search-engine friendly clone of the ACL2 documentation.

Atc-tag-tables

Atc-get-tag-info

Retrieve the information about a tag from a tag table.

Signature
(atc-get-tag-info tag prec-tags) → info
Arguments: tag — Guard (identp tag).; prec-tags — Guard (atc-string-taginfo-alistp prec-tags).
Returns: info — Type (atc-tag-infop 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.

Definitions and Theorems

Function: atc-get-tag-info

(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: atc-tag-infop-of-atc-get-tag-info

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