		Search-engine friendly clone of the ACL2 documentation.

Vl-make-dircache

Vl-make-dircache-aux

Signature
(vl-make-dircache-aux files) → cache
Arguments: files — Guard (string-listp files).
Returns: cache — Type (vl-dircache-p cache).

Definitions and Theorems

Function: vl-make-dircache-aux

(defun vl-make-dircache-aux (files)
  (declare (xargs :guard (string-listp files)))
  (let ((__function__ 'vl-make-dircache-aux))
    (declare (ignorable __function__))
    (if (atom files)
        nil
      (cons (cons (hons-copy (string-fix (car files)))
                  t)
            (vl-make-dircache-aux (cdr files))))))

Theorem: vl-dircache-p-of-vl-make-dircache-aux

(defthm vl-dircache-p-of-vl-make-dircache-aux
  (b* ((cache (vl-make-dircache-aux files)))
    (vl-dircache-p cache))
  :rule-classes :rewrite)

Theorem: vl-make-dircache-aux-of-string-list-fix-files

(defthm vl-make-dircache-aux-of-string-list-fix-files
  (equal (vl-make-dircache-aux (string-list-fix files))
         (vl-make-dircache-aux files)))

Theorem: vl-make-dircache-aux-string-list-equiv-congruence-on-files

(defthm vl-make-dircache-aux-string-list-equiv-congruence-on-files
  (implies (str::string-list-equiv files files-equiv)
           (equal (vl-make-dircache-aux files)
                  (vl-make-dircache-aux files-equiv)))
  :rule-classes :congruence)