		Search-engine friendly clone of the ACL2 documentation.

Lucid

Vl-scopestack-is-portdecl-p

Signature
(vl-scopestack-is-portdecl-p name ss) → portdecl-p
Arguments: name — Name of some variable in this scopestack.
Guard (stringp name).; ss — Guard (vl-scopestack-p ss).
Returns: portdecl-p — Type (booleanp portdecl-p).

Definitions and Theorems

Function: vl-scopestack-is-portdecl-p

(defun vl-scopestack-is-portdecl-p (name ss)
  (declare (xargs :guard (and (stringp name)
                              (vl-scopestack-p ss))))
  (let ((__function__ 'vl-scopestack-is-portdecl-p))
    (declare (ignorable __function__))
    (b* (((mv item item-ss)
          (vl-scopestack-find-item/ss name ss)))
      (and item
           (vl-scopestack-case
                item-ss :null nil :global nil :local
                (if (vl-scope-find-portdecl-fast name item-ss.top)
                    t
                  nil))))))

Theorem: booleanp-of-vl-scopestack-is-portdecl-p

(defthm booleanp-of-vl-scopestack-is-portdecl-p
  (b* ((portdecl-p (vl-scopestack-is-portdecl-p name ss)))
    (booleanp portdecl-p))
  :rule-classes :type-prescription)

Theorem: vl-scopestack-is-portdecl-p-of-str-fix-name

(defthm vl-scopestack-is-portdecl-p-of-str-fix-name
  (equal (vl-scopestack-is-portdecl-p (str-fix name)
                                      ss)
         (vl-scopestack-is-portdecl-p name ss)))

Theorem: vl-scopestack-is-portdecl-p-streqv-congruence-on-name

(defthm vl-scopestack-is-portdecl-p-streqv-congruence-on-name
  (implies (streqv name name-equiv)
           (equal (vl-scopestack-is-portdecl-p name ss)
                  (vl-scopestack-is-portdecl-p name-equiv ss)))
  :rule-classes :congruence)

Theorem: vl-scopestack-is-portdecl-p-of-vl-scopestack-fix-ss

(defthm vl-scopestack-is-portdecl-p-of-vl-scopestack-fix-ss
  (equal (vl-scopestack-is-portdecl-p name (vl-scopestack-fix ss))
         (vl-scopestack-is-portdecl-p name ss)))

Theorem: vl-scopestack-is-portdecl-p-vl-scopestack-equiv-congruence-on-ss

(defthm
   vl-scopestack-is-portdecl-p-vl-scopestack-equiv-congruence-on-ss
  (implies (vl-scopestack-equiv ss ss-equiv)
           (equal (vl-scopestack-is-portdecl-p name ss)
                  (vl-scopestack-is-portdecl-p name ss-equiv)))
  :rule-classes :congruence)