(vl-scan-for-zipinfos dir &key (state 'state)) → (mv infos state)
Function:
(defun vl-scan-for-zipinfos-fn (dir state) (declare (xargs :stobjs (state))) (declare (xargs :guard (stringp dir))) (let ((__function__ 'vl-scan-for-zipinfos)) (declare (ignorable __function__)) (b* (((mv err files state) (oslib::ls-files dir)) ((when err) (cw "; NOTE: Error listing ~x0: ~@1~%" dir err) (mv nil state)) ((mv infos state) (vl-scan-for-zipinfos-aux dir files))) (mv infos state))))
Theorem:
(defthm vl-zipinfolist-p-of-vl-scan-for-zipinfos.infos (b* (((mv ?infos acl2::?state) (vl-scan-for-zipinfos-fn dir state))) (vl-zipinfolist-p infos)) :rule-classes :rewrite)
Theorem:
(defthm state-p1-of-vl-scan-for-zipinfos.state (implies (state-p1 state) (b* (((mv ?infos acl2::?state) (vl-scan-for-zipinfos-fn dir state))) (state-p1 state))) :rule-classes :rewrite)