		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-operations

Transunit-ensemble-paths

Set of file paths in a translation unit ensemble.

Signature
(transunit-ensemble-paths tunits) → paths
Arguments: tunits — Guard (transunit-ensemblep tunits).
Returns: paths — Type (filepath-setp paths).

These are the keys of the map from file paths to translation units.

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

Together with transunit-at-path, it can be used as an API to inspect translation unit ensembles.

Definitions and Theorems

Function: transunit-ensemble-paths

(defun transunit-ensemble-paths (tunits)
  (declare (xargs :guard (transunit-ensemblep tunits)))
  (omap::keys (transunit-ensemble->units tunits)))

Theorem: filepath-setp-of-transunit-ensemble-paths

(defthm filepath-setp-of-transunit-ensemble-paths
  (b* ((paths (transunit-ensemble-paths tunits)))
    (filepath-setp paths))
  :rule-classes :rewrite)

Theorem: transunit-ensemble-paths-of-transunit-ensemble-fix-tunits

(defthm transunit-ensemble-paths-of-transunit-ensemble-fix-tunits
  (equal (transunit-ensemble-paths (transunit-ensemble-fix tunits))
         (transunit-ensemble-paths tunits)))

Theorem: transunit-ensemble-paths-transunit-ensemble-equiv-congruence-on-tunits

(defthm
 transunit-ensemble-paths-transunit-ensemble-equiv-congruence-on-tunits
 (implies (transunit-ensemble-equiv tunits tunits-equiv)
          (equal (transunit-ensemble-paths tunits)
                 (transunit-ensemble-paths tunits-equiv)))
 :rule-classes :congruence)