		Search-engine friendly clone of the ACL2 documentation.

Regaccess

Regaccess->comps

Get the comps field from a regaccess.

Signature
(regaccess->comps x) → comps
Arguments: x — Guard (regaccessp x).
Returns: comps — Type (identifier-listp comps).

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

Definitions and Theorems

Function: regaccess->comps$inline

(defun regaccess->comps$inline (x)
  (declare (xargs :guard (regaccessp x)))
  (declare (xargs :guard t))
  (let ((__function__ 'regaccess->comps))
    (declare (ignorable __function__))
    (mbe :logic
         (b* ((x (and t x)))
           (identifier-list-fix (cdr (std::da-nth 1 (cdr x)))))
         :exec (cdr (std::da-nth 1 (cdr x))))))

Theorem: identifier-listp-of-regaccess->comps

(defthm identifier-listp-of-regaccess->comps
  (b* ((comps (regaccess->comps$inline x)))
    (identifier-listp comps))
  :rule-classes :rewrite)

Theorem: regaccess->comps$inline-of-regaccess-fix-x

(defthm regaccess->comps$inline-of-regaccess-fix-x
  (equal (regaccess->comps$inline (regaccess-fix x))
         (regaccess->comps$inline x)))

Theorem: regaccess->comps$inline-regaccess-equiv-congruence-on-x

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