Lean 4 定理证明

 Lean 4 定理证明

Jeremy AvigadLeonardo de MouraSoonho KongSebastian Ullrich

with contributions from the Lean Community

Lean-zh 项目组 译

本书假定你使用 Lean 4 4.26.0。安装方式参见 Lean 4 中文社区 中的 安装指南 一节。原版指南在这里。 本书的第一版为 Lean 2 编写，Lean 3 版请访问 此处。

Contents

  1. 1. 简介
  2. 2. 依值类型论
  3. 3. 命题与证明
  4. 4. 量词与相等
  5. 5. 证明策略
  6. 6. 与 Lean 交互
  7. 7. 归纳类型
  8. 8. 归纳和递归
  9. 9. 结构体和记录
  10. 10. 类型类
  11. 11. 转换策略模式
  12. 12. 公理与计算