How to write to a file🔗

Writing to a file in Lean can be done using the IO.FS.writeFile function simply. However, another way to create a new file and write a string to it, you can use IO.FS.Handle.mk to create a file handle using a string path and the IO.FS.Mode.write mode to indicate that you want to write to the file. The file has type IO.FS.Handle, which means you are given the handle to the file and can do operations on it.

To write a string to the file, you can use the IO.FS.Handle.putStr method on the file handle. This will overwrite the contents of the file with the string you provide. If the file does not exist, it will be created.

def writeToFile (path : System.FilePath) (s : String)
    : IO Unit := do
  IO.FS.writeFile path s

-- Another way where you use file handle directly
def writeToFile' (path s : String) : IO Unit := do
  let file := ← IO.FS.Handle.mk path IO.FS.Mode.write
  file.putStr s