(parse-fileset-loop filemap) → (mv erp tunitmap)
Function:
(defun parse-fileset-loop (filemap) (declare (xargs :guard (filepath-filedata-mapp filemap))) (let ((__function__ 'parse-fileset-loop)) (declare (ignorable __function__)) (b* (((reterr) nil) ((when (omap::emptyp filemap)) (retok nil)) ((mv filepath filedata) (omap::head filemap)) ((erp tunit) (parse-file filepath (filedata->unwrap filedata))) ((erp tunitmap) (parse-fileset-loop (omap::tail filemap)))) (retok (omap::update (filepath-fix filepath) tunit tunitmap)))))
Theorem:
(defthm filepath-transunit-mapp-of-parse-fileset-loop.tunitmap (b* (((mv acl2::?erp ?tunitmap) (parse-fileset-loop filemap))) (filepath-transunit-mapp tunitmap)) :rule-classes :rewrite)
Theorem:
(defthm keys-of-parse-fileset-loop (implies (filepath-filedata-mapp filemap) (b* (((mv acl2::?erp ?tunitmap) (parse-fileset-loop filemap))) (implies (not erp) (equal (omap::keys tunitmap) (omap::keys filemap))))))