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 adds recipes for other important file formats which are not Data structures, such as JSONL, which are commonly used.

It will be useful to check out Data Structures for File Formats which are Data Structures like JSON, TOML, etc. This chapter uses various IO recipes which you can checkout in I/O chapter beforehand.

Recipes:

1. Reading from a file
2. Writing to a file
3. Creating directories
4. Listing Directory
5. Deleting a file or Directory
6. Read and Set File Permissions
7. Handling JSONL File
8. Miscellaneous FileSystem Usages