Lean 函数式编程

 Lean 函数式编程

David Thrane Christiansen

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

本书是一本关于将 Lean 用作编程语言的免费书籍。所有代码示例均已使用 Lean 发行版 4.26.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. 后续学习