		Search-engine friendly clone of the ACL2 documentation.

Vl-define

Vl-add-define

Add a definition to the defines list.

Signature
(vl-add-define name a x) → new-x
Arguments: name — Guard (stringp name).; a — Guard (vl-define-p a).; x — Guard (vl-defines-p x).
Returns: new-x — Type (vl-defines-p new-x).

Definitions and Theorems

Function: vl-add-define

(defun vl-add-define (name a x)
  (declare (xargs :guard (and (stringp name)
                              (vl-define-p a)
                              (vl-defines-p x))))
  (let ((__function__ 'vl-add-define))
    (declare (ignorable __function__))
    (hons-acons (string-fix name)
                (vl-define-fix a)
                (vl-defines-fix x))))

Theorem: vl-defines-p-of-vl-add-define

(defthm vl-defines-p-of-vl-add-define
  (b* ((new-x (vl-add-define name a x)))
    (vl-defines-p new-x))
  :rule-classes :rewrite)

Theorem: vl-add-define-of-str-fix-name

(defthm vl-add-define-of-str-fix-name
  (equal (vl-add-define (str-fix name) a x)
         (vl-add-define name a x)))

Theorem: vl-add-define-streqv-congruence-on-name

(defthm vl-add-define-streqv-congruence-on-name
  (implies (streqv name name-equiv)
           (equal (vl-add-define name a x)
                  (vl-add-define name-equiv a x)))
  :rule-classes :congruence)

Theorem: vl-add-define-of-vl-define-fix-a

(defthm vl-add-define-of-vl-define-fix-a
  (equal (vl-add-define name (vl-define-fix a) x)
         (vl-add-define name a x)))

Theorem: vl-add-define-vl-define-equiv-congruence-on-a

(defthm vl-add-define-vl-define-equiv-congruence-on-a
  (implies (vl-define-equiv a a-equiv)
           (equal (vl-add-define name a x)
                  (vl-add-define name a-equiv x)))
  :rule-classes :congruence)

Theorem: vl-add-define-of-vl-defines-fix-x

(defthm vl-add-define-of-vl-defines-fix-x
  (equal (vl-add-define name a (vl-defines-fix x))
         (vl-add-define name a x)))

Theorem: vl-add-define-vl-defines-equiv-congruence-on-x

(defthm vl-add-define-vl-defines-equiv-congruence-on-x
  (implies (vl-defines-equiv x x-equiv)
           (equal (vl-add-define name a x)
                  (vl-add-define name a x-equiv)))
  :rule-classes :congruence)