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。 从 帕斯卡三角形 到 电话号码。

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

帕斯卡三角形

帕斯卡三角形

计算帕斯卡三角形，直到给定的行数。

过敏

过敏

给定一个人的过敏评分，判断他是否对某个物品过敏，并列出他完整的过敏清单。

电话号码

电话号码

清理用户输入的电话号码，以便能向这些号码发送短信。

查看 Exercism 上所有 Lean 练习

Lean 的主要功能

Lean

纯函数式

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

依赖类型

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

程序与证明

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

经证明的正确性

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

类型类

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

强大的元编程

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

以 Lean 的方式接受指导

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

了解更多关于指导的内容

由社区贡献的 Lean 练习

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

查看 Lean 的全部练习
Lean

开始学习 Lean 轨道

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

加入 Lean 轨道