Lean 4 (Meta)programming Cookbook

How to delete a file🔗

You can delete a file using IO.FS.removeFile function. It returns an IO Unit which means it performs the action of deleting the file but does not return any value.

def deleteFile (path : String) : IO Unit := do try IO.FS.removeFile path IO.println s!"File {path} deleted successfully." catch e => IO.println s!"Failed to delete file {path}: {e}"