		Search-engine friendly clone of the ACL2 documentation.

Files

Fileset-paths

Set of file paths in a file set.

Signature
(fileset-paths files) → paths
Arguments: files — Guard (filesetp files).
Returns: paths — Type (filepath-setp paths).

These are the keys of the map from file paths to file data.

It is more concise, and more abstract, than extracting the map and then the keys.

Together with file-at-path, it can be used as an API to inspect a file set.

Definitions and Theorems

Function: fileset-paths

(defun fileset-paths (files)
  (declare (xargs :guard (filesetp files)))
  (let ((__function__ 'fileset-paths))
    (declare (ignorable __function__))
    (omap::keys (fileset->unwrap files))))

Theorem: filepath-setp-of-fileset-paths

(defthm filepath-setp-of-fileset-paths
  (b* ((paths (fileset-paths files)))
    (filepath-setp paths))
  :rule-classes :rewrite)

Theorem: fileset-paths-of-fileset-fix-files

(defthm fileset-paths-of-fileset-fix-files
  (equal (fileset-paths (fileset-fix files))
         (fileset-paths files)))

Theorem: fileset-paths-fileset-equiv-congruence-on-files

(defthm fileset-paths-fileset-equiv-congruence-on-files
  (implies (fileset-equiv files files-equiv)
           (equal (fileset-paths files)
                  (fileset-paths files-equiv)))
  :rule-classes :congruence)