		Search-engine friendly clone of the ACL2 documentation.

Indname-result

Indname-result->varname

Get the varname field from a indname-result.

Signature
(indname-result->varname x) → varname
Arguments: x — Guard (indname-result-p x).
Returns: varname — Type (svar-p varname).

This is an ordinary field accessor created by defprod.

Definitions and Theorems

Function: indname-result->varname$inline

(defun indname-result->varname$inline (x)
  (declare (xargs :guard (indname-result-p x)))
  (declare (xargs :guard t))
  (let ((__function__ 'indname-result->varname))
    (declare (ignorable __function__))
    (mbe :logic (b* ((x (and t x))) (svar-fix (car x)))
         :exec (car x))))

Theorem: svar-p-of-indname-result->varname

(defthm svar-p-of-indname-result->varname
  (b* ((varname (indname-result->varname$inline x)))
    (svar-p varname))
  :rule-classes :rewrite)

Theorem: indname-result->varname$inline-of-indname-result-fix-x

(defthm indname-result->varname$inline-of-indname-result-fix-x
  (equal (indname-result->varname$inline (indname-result-fix x))
         (indname-result->varname$inline x)))

Theorem: indname-result->varname$inline-indname-result-equiv-congruence-on-x

(defthm
 indname-result->varname$inline-indname-result-equiv-congruence-on-x
 (implies (indname-result-equiv x x-equiv)
          (equal (indname-result->varname$inline x)
                 (indname-result->varname$inline x-equiv)))
 :rule-classes :congruence)