Delete-file$
Delete a file
This analogue of the Common Lisp function, delete-file, uses
that function under the hood to delete a given file. It returns (mv t
state) if deletion succeeds and (mv nil state) otherwise. The guard of delete-file$ requires that the first argument is a string; the
second argument is the ACL2 state. The logical definition does not
actually look at the file and hence is not useful for reasoning.
Function: delete-file$
(defun delete-file$ (file state)
(declare (xargs :guard (stringp file)
:stobjs state))
(declare (ignore file))
(mv-let (erp val state)
(read-acl2-oracle state)
(declare (ignore val))
(mv (null erp) state)))
