Lean
Lean
关于 Lean练习

想学习并精通 Lean 吗？

加入 Exercism 的 Lean 轨道，即可获得 100 个练习 还会自动分析 你的代码，并提供 个性化指导， 而且全部100% 免费。

加入 Lean 轨道 探索练习

关于 Lean

namespace HelloWorld

inductive World where
    | earth | mars

def hello (world : World) : String :=
    match world with
    | .earth => "Hello, Earth!"
    | .mars  => "Hi, Mars!"

end HelloWorld

100 个编程练习，尽在 Exercism 的 Lean。 从 太空时代 到 Two-Fer。

借助有趣又有收获的编程练习提升编程水平，在 Exercism 上检验你对概念的理解。

太空时代

太空时代

给定一个以秒为单位的年龄，计算某人在给定行星的太阳年中的年龄。

十二天

十二天

输出 'The Twelve Days of Christmas' 的歌词。

Two-Fer

Two-Fer

生成一个形如 "One for X, one for me." 的句子。

查看 Exercism 上所有 Lean 练习

Lean 的主要功能

Lean

纯函数式

确定性的函数让代码更可预测、可组合，也更容易理解。

依赖类型

把规则直接编码进类型里，类型就自带文档，非法状态也无法被表示。

程序与证明

用同一门语言编写程序并证明其正确。规格说明本身就是代码。

经证明的正确性

用数学方法证明代码的关键性质，从而超越单纯的测试。

类型类

将类型归类为类，能带来轻量而可扩展的抽象。

强大的元编程

强大的宏与精化器框架，让你能扩展这门语言，以适应自己的领域。

以 Lean 的方式接受指导

每种语言都有自己的做事方式，Lean 也不例外。我们的导师会帮助你学会像 Lean 开发者那样思考，并教你如何写出地道的 Lean 代码。解完一道练习后，把它提交给我们由志愿者组成的团队，他们会给你提示、想法和反馈，帮你写出更接近 Lean 中常见风格的代码，还会帮你发现那些你并不知道自己不知道的东西。

了解更多关于指导的内容

由社区贡献的 Lean 练习

Exercism 上的 Lean 轨道有 100 个练习，帮你写出更好的代码。

查看 Lean 的全部练习
Lean

开始学习 Lean 轨道

最棒的是，它对所有人 100% 免费。

加入 Lean 轨道