		Search-engine friendly clone of the ACL2 documentation.

Static-semantics

Check-tyname

Check a type name.

Signature
(check-tyname tyname tagenv) → type
Arguments: tyname — Guard (tynamep tyname).; tagenv — Guard (tag-envp tagenv).
Returns: type — Type (type-resultp type).

Return the denoted type if successful. We first check the type specifier sequence, then the abstracto object declarator.

Definitions and Theorems

Function: check-tyname

(defun check-tyname (tyname tagenv)
  (declare (xargs :guard (and (tynamep tyname)
                              (tag-envp tagenv))))
  (let ((__function__ 'check-tyname))
    (declare (ignorable __function__))
    (b* (((okf type)
          (check-tyspecseq (tyname->tyspec tyname)
                           tagenv)))
      (check-obj-adeclor (tyname->declor tyname)
                         type))))

Theorem: type-resultp-of-check-tyname

(defthm type-resultp-of-check-tyname
  (b* ((type (check-tyname tyname tagenv)))
    (type-resultp type))
  :rule-classes :rewrite)

Theorem: check-tyname-of-tyname-fix-tyname

(defthm check-tyname-of-tyname-fix-tyname
  (equal (check-tyname (tyname-fix tyname)
                       tagenv)
         (check-tyname tyname tagenv)))

Theorem: check-tyname-tyname-equiv-congruence-on-tyname

(defthm check-tyname-tyname-equiv-congruence-on-tyname
  (implies (tyname-equiv tyname tyname-equiv)
           (equal (check-tyname tyname tagenv)
                  (check-tyname tyname-equiv tagenv)))
  :rule-classes :congruence)

Theorem: check-tyname-of-tag-env-fix-tagenv

(defthm check-tyname-of-tag-env-fix-tagenv
  (equal (check-tyname tyname (tag-env-fix tagenv))
         (check-tyname tyname tagenv)))

Theorem: check-tyname-tag-env-equiv-congruence-on-tagenv

(defthm check-tyname-tag-env-equiv-congruence-on-tagenv
  (implies (tag-env-equiv tagenv tagenv-equiv)
           (equal (check-tyname tyname tagenv)
                  (check-tyname tyname tagenv-equiv)))
  :rule-classes :congruence)