Lean 4(元)编程 Cookbook

文件系统🔗

贡献者:subfish-zhou

本章覆盖大多数文件系统操作,例如读写文件、创建目录、列出目录内容等。我们主要使用 System.FilePath 类型以及 Lean 标准库中的 IO.FS 模块。 本章还为其他重要但不属于数据结构的文件格式补充了配方,例如常用的 JSONL。

对于像 JSON、TOML 等本身是数据结构的文件格式,可以参阅 数据结构。 本章用到多个 IO 配方,你可以事先在 I/O 一章中了解它们。

配方:

  1. 从文件读取
  2. 写入文件
  3. 创建目录
  4. 列出目录
  5. 删除文件或目录
  6. 读取与设置文件权限
  7. 处理 JSONL 文件
  8. 其他文件系统操作