		Search-engine friendly clone of the ACL2 documentation.

Senv

Senv->identifiers

Get the identifiers field from a senv.

Signature
(senv->identifiers x) → identifiers
Arguments: x — Guard (senvp x).
Returns: identifiers — Type (ident-senvp identifiers).

This is an ordinary field accessor created by fty::defprod.

Definitions and Theorems

Function: senv->identifiers$inline

(defun senv->identifiers$inline (x)
  (declare (xargs :guard (senvp x)))
  (declare (xargs :guard t))
  (let ((__function__ 'senv->identifiers))
    (declare (ignorable __function__))
    (mbe :logic
         (b* ((x (and t x)))
           (ident-senv-fix (cdr (std::da-nth 0 (cdr x)))))
         :exec (cdr (std::da-nth 0 (cdr x))))))

Theorem: ident-senvp-of-senv->identifiers

(defthm ident-senvp-of-senv->identifiers
  (b* ((identifiers (senv->identifiers$inline x)))
    (ident-senvp identifiers))
  :rule-classes :rewrite)

Theorem: senv->identifiers$inline-of-senv-fix-x

(defthm senv->identifiers$inline-of-senv-fix-x
  (equal (senv->identifiers$inline (senv-fix x))
         (senv->identifiers$inline x)))

Theorem: senv->identifiers$inline-senv-equiv-congruence-on-x

(defthm senv->identifiers$inline-senv-equiv-congruence-on-x
  (implies (senv-equiv x x-equiv)
           (equal (senv->identifiers$inline x)
                  (senv->identifiers$inline x-equiv)))
  :rule-classes :congruence)