		Search-engine friendly clone of the ACL2 documentation.

Vl-define

Vl-add-define

Add a definition to the defines list.

Signature
(vl-add-define a x) → new-x
Arguments: 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 (a x)
  (declare (xargs :guard (and (vl-define-p a) (vl-defines-p x))))
  (let ((__function__ 'vl-add-define))
    (declare (ignorable __function__))
    (cons (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 a x)))
    (vl-defines-p new-x))
  :rule-classes :rewrite)

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

(defthm vl-add-define-of-vl-define-fix-a
  (equal (vl-add-define (vl-define-fix a) x)
         (vl-add-define 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 a x)
                  (vl-add-define 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 a (vl-defines-fix x))
         (vl-add-define 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 a x)
                  (vl-add-define a x-equiv)))
  :rule-classes :congruence)