		Search-engine friendly clone of the ACL2 documentation.

Vl-define

Vl-delete-define

Delete an entry from the defines list, if it exists.

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

Definitions and Theorems

Function: vl-delete-define

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

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

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

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

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

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

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

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

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

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

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