Copy files or directories, or cause a hard error.
(copy! from to &key (recursive 'nil) (overwrite 'nil) (limit '1000) (state 'state)) → state
This is identical to copy except that we raise a hard error if anything goes wrong.
Function:
(defun copy!-fn (from to recursive overwrite limit state) (declare (xargs :stobjs (state))) (declare (xargs :guard (and (stringp from) (stringp to) (booleanp recursive) (booleanp overwrite) (natp limit)))) (let ((__function__ 'copy!)) (declare (ignorable __function__)) (b* (((mv err state) (copy from to :recursive recursive :overwrite overwrite :limit limit)) ((when err) (raise "~@0" err) state)) state)))
Theorem:
(defthm state-p1-of-copy! (implies (force (state-p1 state)) (b* ((state (copy!-fn from to recursive overwrite limit state))) (state-p1 state))) :rule-classes :rewrite)