		Search-engine friendly clone of the ACL2 documentation.

Address

Svar->address

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

Definitions and Theorems

Function: svar->address

(defun svar->address (x)
  (declare (xargs :guard (svar-p x)))
  (declare (xargs :guard (svar-addr-p x)))
  (let ((__function__ 'svar->address))
    (declare (ignorable __function__))
    (address-fix (svar->name x))))

Theorem: address-p-of-svar->address

(defthm address-p-of-svar->address
  (b* ((address (svar->address x)))
    (address-p address))
  :rule-classes :rewrite)

Theorem: svar->address-of-address->svar

(defthm svar->address-of-address->svar
  (equal (svar->address (address->svar x))
         (address-fix x)))

Theorem: svar->address-of-svar-fix-x

(defthm svar->address-of-svar-fix-x
  (equal (svar->address (svar-fix x))
         (svar->address x)))

Theorem: svar->address-svar-equiv-congruence-on-x

(defthm svar->address-svar-equiv-congruence-on-x
  (implies (svar-equiv x x-equiv)
           (equal (svar->address x)
                  (svar->address x-equiv)))
  :rule-classes :congruence)