		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)