		Search-engine friendly clone of the ACL2 documentation.

Address

Make-simple-svar

Signature
(make-simple-svar name) → var
Arguments: name — Guard (name-p name).
Returns: var — Type (and (svar-p var) (svar-addr-p var)).

Definitions and Theorems

Function: make-simple-svar

(defun make-simple-svar (name)
 (declare (xargs :guard (name-p name)))
 (let ((__function__ 'make-simple-svar))
  (declare (ignorable __function__))
  (address->svar (make-address :path (make-path-wire :name name)))))

Theorem: return-type-of-make-simple-svar

(defthm return-type-of-make-simple-svar
  (b* ((var (make-simple-svar name)))
    (and (svar-p var) (svar-addr-p var)))
  :rule-classes :rewrite)

Theorem: make-simple-svar-of-name-fix-name

(defthm make-simple-svar-of-name-fix-name
  (equal (make-simple-svar (name-fix name))
         (make-simple-svar name)))

Theorem: make-simple-svar-name-equiv-congruence-on-name

(defthm make-simple-svar-name-equiv-congruence-on-name
  (implies (name-equiv name name-equiv)
           (equal (make-simple-svar name)
                  (make-simple-svar name-equiv)))
  :rule-classes :congruence)