此版本添加了关于应用函子的章节，此外还更加详细地描述了结构和类型类。此外改进了对单子的描述。由于冬季假期，2022 年 12 月版本被推迟到 2023 年 1 月。
此版本添加了关于使用单子编程的章节。此外，强制转换一节中使用 JSON 的示例已更新为包含完整代码。
此版本完成了类型类的章节。此外，在类型类章节之前添加了一个简短的插曲，介绍了命题、证明和策略，因为简单了解一下这些概念有助于理解一些标准库中的类型类。
此版本添加了一个关于类型类的章节的前半部分，这是 Lean 的运算符重载机制，也是组织代码和构建函数库的重要手段。此外，还更新了第二章以适应 Lean 中 Stream 流 API 的变化。
第三次公开发布增加了第二章，其中描述了编译和运行程序以及 Lean 的副作用模型。
第二次公开发布，完成了第一章。
这是第一次公开发布，包括引言和第一章的一部分。
David Thrane Christiansen 已使用函数式语言二十年，并使用依值类型十年。他与 Daniel P. Friedman 合著了《
The Little Typer
》，介绍了依值类型论的关键思想。他拥有哥本哈根 IT 大学的博士学位。在学习期间，他为 Idris 语言的第一个版本做出了重大贡献。离开学术界后，他曾在俄勒冈州波特兰的 Galois 和丹麦哥本哈根的 Deon Digital 担任软件开发人员，并担任 Haskell 基金会执行董事。在撰写本文时，他受雇于
Lean 专注研究组织
，全职从事 Lean 的工作。"
本作品采用
知识共享-署名 4.0 国际许可协议
授权。
