File System🔗

This chapter covers most FileSystem operations, such as reading and writing files, creating directories, listing directory contents, etc. We mainly use the System.FilePath type and the IO.FS module from the Lean standard library.

This chapter also adds recipes for other important file formats, such as JSONL, which are commonly used.

1. Reading from a file
2. Writing to a file
3. Creating directories
4. Listing Directory
5. Deleting a file or Directory
6. Running an external program
7. Handling JSONL File
8. Miscellaneous FileSystem Usages