Set of file paths in a translation unit ensemble.
(transunit-ensemble-paths tunits) → 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.
Function:
(defun transunit-ensemble-paths (tunits) (declare (xargs :guard (transunit-ensemblep tunits))) (let ((__function__ 'transunit-ensemble-paths)) (declare (ignorable __function__)) (omap::keys (transunit-ensemble->unwrap tunits))))
Theorem:
(defthm filepath-setp-of-transunit-ensemble-paths (b* ((paths (transunit-ensemble-paths tunits))) (filepath-setp paths)) :rule-classes :rewrite)
Theorem:
(defthm transunit-ensemble-paths-of-transunit-ensemble-fix-tunits (equal (transunit-ensemble-paths (transunit-ensemble-fix tunits)) (transunit-ensemble-paths tunits)))
Theorem:
(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)