		Search-engine friendly clone of the ACL2 documentation.

Vl-delta-p

Vl-free-delta

Frees the namefactory within a vl-delta-p and returns delta.

Signature
(vl-free-delta delta) → delta
Arguments: delta — Guard (vl-delta-p delta).
Returns: delta — Type (vl-delta-p delta).

Definitions and Theorems

Function: vl-free-delta

(defun vl-free-delta (delta)
  (declare (xargs :guard (vl-delta-p delta)))
  (let ((__function__ 'vl-free-delta))
    (declare (ignorable __function__))
    (b* (((vl-delta delta) delta))
      (vl-free-namefactory delta.nf)
      (vl-delta-fix delta))))

Theorem: vl-delta-p-of-vl-free-delta

(defthm vl-delta-p-of-vl-free-delta
  (b* ((delta (vl-free-delta delta)))
    (vl-delta-p delta))
  :rule-classes :rewrite)

Theorem: vl-free-delta-of-vl-delta-fix-delta

(defthm vl-free-delta-of-vl-delta-fix-delta
  (equal (vl-free-delta (vl-delta-fix delta))
         (vl-free-delta delta)))

Theorem: vl-free-delta-vl-delta-equiv-congruence-on-delta

(defthm vl-free-delta-vl-delta-equiv-congruence-on-delta
  (implies (vl-delta-equiv delta delta-equiv)
           (equal (vl-free-delta delta)
                  (vl-free-delta delta-equiv)))
  :rule-classes :congruence)