		Search-engine friendly clone of the ACL2 documentation.

Compile.lisp

Assigns-to-overrides

Signature
(assigns-to-overrides x) → override
Arguments: x — Guard (assigns-p x).
Returns: override — Type (lhs-overridelist-p override).

Definitions and Theorems

Function: assigns-to-overrides

(defun assigns-to-overrides (x)
  (declare (xargs :guard (assigns-p x)))
  (let ((__function__ 'assigns-to-overrides))
    (declare (ignorable __function__))
    (mbe :logic
         (b* ((x (assigns-fix x))
              ((when (atom x)) nil)
              ((cons lhs (driver rhs)) (car x))
              (ans (make-lhs-override :lhs lhs
                                      :test 1
                                      :val rhs.value)))
           (cons ans (assigns-to-overrides (cdr x))))
         :exec
         (if (atom x)
             nil
           (acl2::with-local-nrev
                (assigns-to-overrides-nrev x acl2::nrev))))))

Theorem: lhs-overridelist-p-of-assigns-to-overrides

(defthm lhs-overridelist-p-of-assigns-to-overrides
  (b* ((override (assigns-to-overrides x)))
    (lhs-overridelist-p override))
  :rule-classes :rewrite)

Theorem: vars-of-assigns-to-overrides

(defthm vars-of-assigns-to-overrides
  (b* ((?override (assigns-to-overrides x)))
    (implies
         (not (member v (assigns-vars x)))
         (and (not (member v (lhs-overridelist-vars override)))
              (not (member v (lhs-overridelist-keys override)))))))

Theorem: assigns-to-overrides-of-assigns-fix-x

(defthm assigns-to-overrides-of-assigns-fix-x
  (equal (assigns-to-overrides (assigns-fix x))
         (assigns-to-overrides x)))

Theorem: assigns-to-overrides-assigns-equiv-congruence-on-x

(defthm assigns-to-overrides-assigns-equiv-congruence-on-x
  (implies (assigns-equiv x x-equiv)
           (equal (assigns-to-overrides x)
                  (assigns-to-overrides x-equiv)))
  :rule-classes :congruence)