Lean 4（元）编程 Cookbook

索引🔗

Symbols

  1. “Hello World” 命令
  2. 为命令添加语法
  3. 为子进程设置环境变量
  4. 为项添加语法
  5. 二叉搜索树
  6. 二叉树上的操作
  7. 从 JSON 读取值
  8. 从 Stdin 读取
  9. 从 TOML 读取值
  10. 从函数应用构造表达式
  11. 从文件读取
  12. 代码、语法与表达式
  13. 任务系统中的阻塞与资源耗尽
  14. 使用 HashMap 做记忆化
  15. 修改 JSON 对象
  16. 修改 TOML 对象
  17. 修改目标
  18. 写入 JSON 文件
  19. 写入 JSONL 文件
  20. 写入 TOML 文件
  21. 写入文件
  22. 准引用：创建与匹配语法
  23. 函数、依值函数与函数类型的表达式
  24. 列出目录的内容
  25. 列表转二叉树
  26. 创建目录
  27. 删除文件
  28. 删除目录
  29. 反复应用定理的策略
  30. 可中断的休眠
  31. 可变变量：示例
  32. 向文件追加
  33. 在信息视图中显示
  34. 声明一个语法类别
  35. 处理 JSON 文件
  36. 处理 JSONL 文件
  37. 处理 Json 对象
  38. 处理嵌套 TOML
  39. 如何编写配方
  40. 定义二叉树
  41. 实践中的单子
  42. 并行运行任务
  43. 异步休眠
  44. 性能计时
  45. 打印主目标的策略
  46. 打印到 Stdout 和 Stderr
  47. 把 JSON 转换成 TOML
  48. 把 TOML 转换成 JSON
  49. 把策略当作快捷方式
  50. 拼接文件路径
  51. 文件压缩与解压
  52. 更新 lakefile.toml
  53. 替换为可行的策略
  54. 查看与关闭目标
  55. 检查文件大小
  56. 检查某个命题是否能被 grind 解决的命令
  57. 检查策略
  58. 检查路径是绝对路径还是相对路径
  59. 检查路径的元数据
  60. 派生任务与工作线程
  61. 派生子进程
  62. 添加语法（类别）
  63. 状态单子：记住计算结果
  64. 环境扩展与属性
  65. 环境扩展与属性：示例
  66. 用 RBMap 调度进程
  67. 用 RBTree 追踪未定义的标识符
  68. 直接对表达式进行模式匹配
  69. 终止一个进程
  70. 编写一个宏
  71. 编码 TOML
  72. 获取一个随机数
  73. 获取当前工作目录
  74. 获取线程 ID
  75. 获取进程的 PID
  76. 表达式的种类
  77. 覆盖 CLI 行
  78. 解析 TOML
  79. 解析 lakefile.toml
  80. 解析命令行参数
  81. 让进程休眠
  82. 设置文件权限
  83. 证明自然数不等式的策略
  84. 读取 JSON 文件
  85. 读取 JSONL 文件
  86. 读取 TOML 文件
  87. 读取与设置文件权限
  88. 读取嵌套 TOML
  89. 读取环境变量
  90. 跨命令的可变变量
  91. 进度条与旋转指示符
  92. 进程空闲休眠
  93. 递归遍历目录
  94. 通过求解对表达式进行模式匹配
  95. 遍历目录树
  96. 重命名文件路径
  97. 高级 HashMap 操作

A

  1. ANSI 颜色
  2. add
    1. Nat.add

H

  1. HTML 无序列表的 DSL
  2. HashMap 基本操作
  3. Hello World 策略

I

  1. I/O 与进程
  2. IO.asTask 与 BaseIO.asTask

J

  1. Json 处理默认值
  2. Json 字段重命名

L

  1. log­Error
  2. log­Info
  3. log­Warning

N

  1. Nat.add

P

  1. Python for 循环 DSL
  2. Python 幂运算 DSL

R

  1. RBMap 操作
  2. RBTree 基本操作