Lean 4 (Meta)programming Cookbook

How to delete a directory🔗

You can delete a directory using IO.FS.removeDir function to delete an empty directory. If you want to delete all the contents inside the directory, use IO.FS.removeDirAll

def deleteEmptyDir (path : String) : IO Unit := do IO.FS.removeDir path def deleteDir (path: String) : IO Unit := do IO.FS.removeDirAll path

Refer to Creating directories section bottom to know more about why String works as a file path here.