		Search-engine friendly clone of the ACL2 documentation.

Static-environments

Add-struct-sinfo

Add information about a struct type to a static environment.

Signature
(add-struct-sinfo circ info env) → new-env
Arguments: circ — Guard (identifierp circ).; info — Guard (struct-sinfop info).; env — Guard (senvp env).
Returns: new-env — Type (senv-optionp new-env).

Definitions and Theorems

Function: add-struct-sinfo

(defun add-struct-sinfo (circ info env)
  (declare (xargs :guard (and (identifierp circ)
                              (struct-sinfop info)
                              (senvp env))))
  (let ((__function__ 'add-struct-sinfo))
    (declare (ignorable __function__))
    (add-ident-sinfo circ (ident-sinfo-struct info)
                     env)))

Theorem: senv-optionp-of-add-struct-sinfo

(defthm senv-optionp-of-add-struct-sinfo
  (b* ((new-env (add-struct-sinfo circ info env)))
    (senv-optionp new-env))
  :rule-classes :rewrite)

Theorem: add-struct-sinfo-of-identifier-fix-circ

(defthm add-struct-sinfo-of-identifier-fix-circ
  (equal (add-struct-sinfo (identifier-fix circ)
                           info env)
         (add-struct-sinfo circ info env)))

Theorem: add-struct-sinfo-identifier-equiv-congruence-on-circ

(defthm add-struct-sinfo-identifier-equiv-congruence-on-circ
  (implies (identifier-equiv circ circ-equiv)
           (equal (add-struct-sinfo circ info env)
                  (add-struct-sinfo circ-equiv info env)))
  :rule-classes :congruence)

Theorem: add-struct-sinfo-of-struct-sinfo-fix-info

(defthm add-struct-sinfo-of-struct-sinfo-fix-info
  (equal (add-struct-sinfo circ (struct-sinfo-fix info)
                           env)
         (add-struct-sinfo circ info env)))

Theorem: add-struct-sinfo-struct-sinfo-equiv-congruence-on-info

(defthm add-struct-sinfo-struct-sinfo-equiv-congruence-on-info
  (implies (struct-sinfo-equiv info info-equiv)
           (equal (add-struct-sinfo circ info env)
                  (add-struct-sinfo circ info-equiv env)))
  :rule-classes :congruence)

Theorem: add-struct-sinfo-of-senv-fix-env

(defthm add-struct-sinfo-of-senv-fix-env
  (equal (add-struct-sinfo circ info (senv-fix env))
         (add-struct-sinfo circ info env)))

Theorem: add-struct-sinfo-senv-equiv-congruence-on-env

(defthm add-struct-sinfo-senv-equiv-congruence-on-env
  (implies (senv-equiv env env-equiv)
           (equal (add-struct-sinfo circ info env)
                  (add-struct-sinfo circ info env-equiv)))
  :rule-classes :congruence)