本章覆盖大多数文件系统操作,例如读写文件、创建目录、列出目录内容等。我们主要使用 System.FilePath 类型以及 Lean 标准库中的 IO.FS 模块。 本章还为其他重要但不属于数据结构的文件格式补充了配方,例如常用的 JSONL。
System.FilePath
IO.FS
对于像 JSON、TOML 等本身是数据结构的文件格式,可以参阅 数据结构。 本章用到多个 IO 配方,你可以事先在 I/O 一章中了解它们。
IO
配方: