Recursively delete files, like the shell command
(rmtree dir &optional (state 'state)) → (mv successp state)
In the logic this function reads from the ACL2 oracle to determine if it succeeds. In the execution, we attempt to delete the requested path, and detect errors.
(defun rmtree-fn (dir state) (declare (xargs :stobjs (state))) (declare (xargs :guard (stringp dir))) (let ((__function__ 'rmtree)) (declare (ignorable __function__)) (b* ((- (raise "Raw Lisp definition not installed?")) ((mv err val state) (read-acl2-oracle state)) (okp (and (not err) (booleanp val) val))) (mv okp state))))
(defthm booleanp-of-rmtree.successp (b* (((mv ?successp acl2::?state) (rmtree-fn dir state))) (booleanp successp)) :rule-classes :type-prescription)
(defthm state-p1-of-rmtree.state (implies (force (state-p1 state)) (b* (((mv ?successp acl2::?state) (rmtree-fn dir state))) (state-p1 state))) :rule-classes :rewrite)