		Search-engine friendly clone of the ACL2 documentation.

File-layout

Vl-scan-for-tnames-in-base

Signature
(vl-scan-for-tnames-in-base base state) → (mv tnames state)
Arguments: base — Guard (stringp base).
Returns: tnames — Type (vl-tnamelist-p tnames).; state — Type (state-p1 state), given (force (state-p1 state)).

Definitions and Theorems

Function: vl-scan-for-tnames-in-base

(defun vl-scan-for-tnames-in-base (base state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (stringp base)))
  (let ((__function__ 'vl-scan-for-tnames-in-base))
    (declare (ignorable __function__))
    (b* ((dir (cat *vls-root* "/" base))
         ((mv err models state)
          (oslib::ls-subdirs dir))
         ((when err)
          (raise "Error listing directory ~x0: ~@1~%"
                 dir err)
          (mv nil state)))
      (mv (vl-scan-for-tnames-in-base-aux base models)
          state))))

Theorem: vl-tnamelist-p-of-vl-scan-for-tnames-in-base.tnames

(defthm vl-tnamelist-p-of-vl-scan-for-tnames-in-base.tnames
  (b* (((mv ?tnames acl2::?state)
        (vl-scan-for-tnames-in-base base state)))
    (vl-tnamelist-p tnames))
  :rule-classes :rewrite)

Theorem: state-p1-of-vl-scan-for-tnames-in-base.state

(defthm state-p1-of-vl-scan-for-tnames-in-base.state
  (implies (force (state-p1 state))
           (b* (((mv ?tnames acl2::?state)
                 (vl-scan-for-tnames-in-base base state)))
             (state-p1 state)))
  :rule-classes :rewrite)

Theorem: true-listp-of-vl-scan-for-tnames-in-base.tnames

(defthm true-listp-of-vl-scan-for-tnames-in-base.tnames
  (b* (((mv ?tnames acl2::?state)
        (vl-scan-for-tnames-in-base base state)))
    (true-listp tnames))
  :rule-classes :type-prescription)

Subtopics

Vl-scan-for-tnames-in-base-aux: Convert the directory listing into a list of tnames.