		Search-engine friendly clone of the ACL2 documentation.

Lucid

Vl-scopestack->flat-transitive-names-slow

Signature
(vl-scopestack->flat-transitive-names-slow ss) → names
Arguments: ss — Guard (vl-scopestack-p ss).
Returns: names — Type (and (string-listp names) (setp names)).

Definitions and Theorems

Function: vl-scopestack->flat-transitive-names-slow

(defun vl-scopestack->flat-transitive-names-slow (ss)
 (declare (xargs :guard (vl-scopestack-p ss)))
 (let ((__function__ 'vl-scopestack->flat-transitive-names-slow))
  (declare (ignorable __function__))
  (vl-scopestack-case
   ss
   :null nil
   :global (mergesort (vl-scope-namespace ss.design ss.design))
   :local
   (union
        (mergesort
             (vl-scope-namespace ss.top (vl-scopestack->design ss)))
        (vl-scopestack->flat-transitive-names-slow ss.super)))))

Theorem: return-type-of-vl-scopestack->flat-transitive-names-slow

(defthm return-type-of-vl-scopestack->flat-transitive-names-slow
  (b* ((names (vl-scopestack->flat-transitive-names-slow ss)))
    (and (string-listp names) (setp names)))
  :rule-classes :rewrite)

Theorem: vl-scopestack->flat-transitive-names-slow-of-vl-scopestack-fix-ss

(defthm
  vl-scopestack->flat-transitive-names-slow-of-vl-scopestack-fix-ss
 (equal
  (vl-scopestack->flat-transitive-names-slow (vl-scopestack-fix ss))
  (vl-scopestack->flat-transitive-names-slow ss)))

Theorem: vl-scopestack->flat-transitive-names-slow-vl-scopestack-equiv-congruence-on-ss

(defthm
 vl-scopestack->flat-transitive-names-slow-vl-scopestack-equiv-congruence-on-ss
 (implies
      (vl-scopestack-equiv ss ss-equiv)
      (equal (vl-scopestack->flat-transitive-names-slow ss)
             (vl-scopestack->flat-transitive-names-slow ss-equiv)))
 :rule-classes :congruence)