		Search-engine friendly clone of the ACL2 documentation.

Lhs.lisp

Svar-index

Signature
(svar-index x) → idx
Arguments: x — Guard (svar-p x).
Returns: idx — Type (natp idx).

Definitions and Theorems

Function: svar-index$inline

(defun svar-index$inline (x)
  (declare (xargs :guard (svar-p x)))
  (declare (xargs :guard (svar-indexedp x)))
  (let ((__function__ 'svar-index))
    (declare (ignorable __function__))
    (lnfix (svar->name x))))

Theorem: natp-of-svar-index

(defthm natp-of-svar-index
  (b* ((idx (svar-index$inline x)))
    (natp idx))
  :rule-classes :type-prescription)

Theorem: svar-index$inline-of-svar-fix-x

(defthm svar-index$inline-of-svar-fix-x
  (equal (svar-index$inline (svar-fix x))
         (svar-index$inline x)))

Theorem: svar-index$inline-svar-equiv-congruence-on-x

(defthm svar-index$inline-svar-equiv-congruence-on-x
  (implies (svar-equiv x x-equiv)
           (equal (svar-index$inline x)
                  (svar-index$inline x-equiv)))
  :rule-classes :congruence)