		Search-engine friendly clone of the ACL2 documentation.

Compile.lisp

Assigns-to-overrides-nrev

Signature
(assigns-to-overrides-nrev x nrev) → nrev
Arguments: x — Guard (assigns-p x).

Definitions and Theorems

Function: assigns-to-overrides-nrev

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

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

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

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

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