		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-collect-idents

Filepath-transunit-map-collect-idents

Signature
(filepath-transunit-map-collect-idents c$::filepath-transunit-map) → fty::result
Arguments: c$::filepath-transunit-map — Guard (filepath-transunit-mapp c$::filepath-transunit-map).
Returns: fty::result — Type (ident-setp fty::result).

Definitions and Theorems

Function: filepath-transunit-map-collect-idents

(defun filepath-transunit-map-collect-idents
       (c$::filepath-transunit-map)
 (declare
  (xargs
       :guard (filepath-transunit-mapp c$::filepath-transunit-map)))
 (let ((__function__ 'filepath-transunit-map-collect-idents))
  (declare (ignorable __function__))
  (cond
   ((not (mbt (filepath-transunit-mapp c$::filepath-transunit-map)))
    nil)
   ((omap::emptyp c$::filepath-transunit-map)
    nil)
   (t (union (transunit-collect-idents
                  (omap::head-val c$::filepath-transunit-map))
             (filepath-transunit-map-collect-idents
                  (omap::tail c$::filepath-transunit-map)))))))

Theorem: ident-setp-of-filepath-transunit-map-collect-idents

(defthm ident-setp-of-filepath-transunit-map-collect-idents
  (b* ((fty::result (filepath-transunit-map-collect-idents
                         c$::filepath-transunit-map)))
    (ident-setp fty::result))
  :rule-classes :rewrite)

Theorem: filepath-transunit-map-collect-idents-of-filepath-transunit-map-fix-filepath-transunit-map

(defthm
 filepath-transunit-map-collect-idents-of-filepath-transunit-map-fix-filepath-transunit-map
 (equal
   (filepath-transunit-map-collect-idents
        (c$::filepath-transunit-map-fix c$::filepath-transunit-map))
   (filepath-transunit-map-collect-idents
        c$::filepath-transunit-map)))

Theorem: filepath-transunit-map-collect-idents-filepath-transunit-map-equiv-congruence-on-filepath-transunit-map

(defthm
 filepath-transunit-map-collect-idents-filepath-transunit-map-equiv-congruence-on-filepath-transunit-map
 (implies
     (c$::filepath-transunit-map-equiv c$::filepath-transunit-map
                                       filepath-transunit-map-equiv)
     (equal (filepath-transunit-map-collect-idents
                 c$::filepath-transunit-map)
            (filepath-transunit-map-collect-idents
                 filepath-transunit-map-equiv)))
 :rule-classes :congruence)