		Search-engine friendly clone of the ACL2 documentation.

Lucid

Vl-lucid-valid-bits-for-decl

Signature
(vl-lucid-valid-bits-for-decl item ss) → (mv simple-p bits)
Arguments: item — Guard (or (vl-paramdecl-p item) (vl-vardecl-p item)).; ss — Guard (vl-scopestack-p ss).
Returns: simple-p — Type (booleanp simple-p).; bits — Type (and (integer-listp bits) (setp bits)).

Definitions and Theorems

Function: vl-lucid-valid-bits-for-decl

(defun vl-lucid-valid-bits-for-decl (item ss)
 (declare (xargs :guard (and (or (vl-paramdecl-p item)
                                 (vl-vardecl-p item))
                             (vl-scopestack-p ss))))
 (let ((__function__ 'vl-lucid-valid-bits-for-decl))
  (declare (ignorable __function__))
  (b*
   ((datatype-for-indexing
        (b* (((when (eq (tag item) :vl-vardecl))
              (vl-vardecl->type item))
             (paramtype (vl-paramdecl->type item)))
          (vl-paramtype-case paramtype (:vl-implicitvalueparam nil)
                             (:vl-explicitvalueparam paramtype.type)
                             (:vl-typeparam nil))))
    ((when datatype-for-indexing)
     (vl-lucid-valid-bits-for-datatype
          datatype-for-indexing ss item)))
   (mv nil nil))))

Theorem: booleanp-of-vl-lucid-valid-bits-for-decl.simple-p

(defthm booleanp-of-vl-lucid-valid-bits-for-decl.simple-p
  (b* (((mv ?simple-p ?bits)
        (vl-lucid-valid-bits-for-decl item ss)))
    (booleanp simple-p))
  :rule-classes :type-prescription)

Theorem: return-type-of-vl-lucid-valid-bits-for-decl.bits

(defthm return-type-of-vl-lucid-valid-bits-for-decl.bits
  (b* (((mv ?simple-p ?bits)
        (vl-lucid-valid-bits-for-decl item ss)))
    (and (integer-listp bits) (setp bits)))
  :rule-classes :rewrite)

Theorem: vl-lucid-valid-bits-for-decl-of-vl-scopestack-fix-ss

(defthm vl-lucid-valid-bits-for-decl-of-vl-scopestack-fix-ss
  (equal (vl-lucid-valid-bits-for-decl item (vl-scopestack-fix ss))
         (vl-lucid-valid-bits-for-decl item ss)))

Theorem: vl-lucid-valid-bits-for-decl-vl-scopestack-equiv-congruence-on-ss

(defthm
  vl-lucid-valid-bits-for-decl-vl-scopestack-equiv-congruence-on-ss
  (implies (vl-scopestack-equiv ss ss-equiv)
           (equal (vl-lucid-valid-bits-for-decl item ss)
                  (vl-lucid-valid-bits-for-decl item ss-equiv)))
  :rule-classes :congruence)