		Search-engine friendly clone of the ACL2 documentation.

Lucid

Vl-lucidocclist-drop-foreign-writes

Signature
(vl-lucidocclist-drop-foreign-writes x decl-ss) → new-s
Arguments: x — Guard (vl-lucidocclist-p x).; decl-ss — Guard (vl-scopestack-p decl-ss).
Returns: new-s — Type (vl-lucidocclist-p new-s).

Definitions and Theorems

Function: vl-lucidocclist-drop-foreign-writes

(defun vl-lucidocclist-drop-foreign-writes (x decl-ss)
  (declare (xargs :guard (and (vl-lucidocclist-p x)
                              (vl-scopestack-p decl-ss))))
  (let ((__function__ 'vl-lucidocclist-drop-foreign-writes))
    (declare (ignorable __function__))
    (b* (((when (atom x)) nil)
         (ss1 (vl-lucidocc->ss (car x)))
         ((unless (vl-lucid-scopestack-subscope-p ss1 decl-ss))
          (vl-lucidocclist-drop-foreign-writes (cdr x)
                                               decl-ss)))
      (cons (vl-lucidocc-fix (car x))
            (vl-lucidocclist-drop-foreign-writes (cdr x)
                                                 decl-ss)))))

Theorem: vl-lucidocclist-p-of-vl-lucidocclist-drop-foreign-writes

(defthm vl-lucidocclist-p-of-vl-lucidocclist-drop-foreign-writes
  (b* ((new-s (vl-lucidocclist-drop-foreign-writes x decl-ss)))
    (vl-lucidocclist-p new-s))
  :rule-classes :rewrite)

Theorem: vl-lucidocclist-drop-foreign-writes-of-vl-lucidocclist-fix-x

(defthm vl-lucidocclist-drop-foreign-writes-of-vl-lucidocclist-fix-x
 (equal (vl-lucidocclist-drop-foreign-writes (vl-lucidocclist-fix x)
                                             decl-ss)
        (vl-lucidocclist-drop-foreign-writes x decl-ss)))

Theorem: vl-lucidocclist-drop-foreign-writes-vl-lucidocclist-equiv-congruence-on-x

(defthm
 vl-lucidocclist-drop-foreign-writes-vl-lucidocclist-equiv-congruence-on-x
 (implies
      (vl-lucidocclist-equiv x x-equiv)
      (equal (vl-lucidocclist-drop-foreign-writes x decl-ss)
             (vl-lucidocclist-drop-foreign-writes x-equiv decl-ss)))
 :rule-classes :congruence)

Theorem: vl-lucidocclist-drop-foreign-writes-of-vl-scopestack-fix-decl-ss

(defthm
   vl-lucidocclist-drop-foreign-writes-of-vl-scopestack-fix-decl-ss
  (equal (vl-lucidocclist-drop-foreign-writes
              x (vl-scopestack-fix decl-ss))
         (vl-lucidocclist-drop-foreign-writes x decl-ss)))

Theorem: vl-lucidocclist-drop-foreign-writes-vl-scopestack-equiv-congruence-on-decl-ss

(defthm
 vl-lucidocclist-drop-foreign-writes-vl-scopestack-equiv-congruence-on-decl-ss
 (implies
      (vl-scopestack-equiv decl-ss decl-ss-equiv)
      (equal (vl-lucidocclist-drop-foreign-writes x decl-ss)
             (vl-lucidocclist-drop-foreign-writes x decl-ss-equiv)))
 :rule-classes :congruence)