		Search-engine friendly clone of the ACL2 documentation.

Lucid

Vl-custom-suppress-multidrive-p-default

Signature
(vl-custom-suppress-multidrive-p-default ss item set) → *
Arguments: ss — Guard (vl-scopestack-p ss).; item — Guard (or (vl-paramdecl-p item) (vl-vardecl-p item)).; set — Guard (vl-lucidocclist-p set).

Definitions and Theorems

Function: vl-custom-suppress-multidrive-p-default

(defun vl-custom-suppress-multidrive-p-default (ss item set)
  (declare (xargs :guard (and (vl-scopestack-p ss)
                              (or (vl-paramdecl-p item)
                                  (vl-vardecl-p item))
                              (vl-lucidocclist-p set))))
  (declare (ignorable ss item set))
  (let ((__function__ 'vl-custom-suppress-multidrive-p-default))
    (declare (ignorable __function__))
    nil))

Theorem: vl-custom-suppress-multidrive-p-default-of-vl-scopestack-fix-ss

(defthm
    vl-custom-suppress-multidrive-p-default-of-vl-scopestack-fix-ss
 (equal
     (vl-custom-suppress-multidrive-p-default (vl-scopestack-fix ss)
                                              item set)
     (vl-custom-suppress-multidrive-p-default ss item set)))

Theorem: vl-custom-suppress-multidrive-p-default-vl-scopestack-equiv-congruence-on-ss

(defthm
 vl-custom-suppress-multidrive-p-default-vl-scopestack-equiv-congruence-on-ss
 (implies
  (vl-scopestack-equiv ss ss-equiv)
  (equal
       (vl-custom-suppress-multidrive-p-default ss item set)
       (vl-custom-suppress-multidrive-p-default ss-equiv item set)))
 :rule-classes :congruence)

Theorem: vl-custom-suppress-multidrive-p-default-of-vl-lucidocclist-fix-set

(defthm
 vl-custom-suppress-multidrive-p-default-of-vl-lucidocclist-fix-set
 (equal (vl-custom-suppress-multidrive-p-default
             ss item (vl-lucidocclist-fix set))
        (vl-custom-suppress-multidrive-p-default ss item set)))

Theorem: vl-custom-suppress-multidrive-p-default-vl-lucidocclist-equiv-congruence-on-set

(defthm
 vl-custom-suppress-multidrive-p-default-vl-lucidocclist-equiv-congruence-on-set
 (implies
  (vl-lucidocclist-equiv set set-equiv)
  (equal
       (vl-custom-suppress-multidrive-p-default ss item set)
       (vl-custom-suppress-multidrive-p-default ss item set-equiv)))
 :rule-classes :congruence)