Lean 函数式编程

 Lean 函数式编程🔗

David Thrane Christiansen

译者：Oling Cat，Qiu233，JiechengZhao，Subfish Zhou

版权所有 Microsoft Corporation 2023 和 Lean FRO, LLC 2023–2025

这是一本关于将 Lean 作为编程语言使用的免费书籍。所有代码示例都使用 Lean 版本 4.23.0 进行测试。

Contents

  1. 简介
  2. 致谢
  3. 1. 了解 Lean
  4. 2. Hello, World!
  5. 插曲：命题、证明与索引
  6. 3. 重载与类型类
  7. 4. 单子
  8. 5. 函子、应用函子和单子
  9. 6. 单子转换器
  10. 7. 使用依值类型编程
  11. 插曲：策略、归纳与证明
  12. 8. 编程、证明与性能
  13. 9. 继续学习