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

在 Exercism 上，Lean 共有100 個程式設計練習。 從 質因數 到 倍數之和。

透過 Exercism 上有趣又有成就感的程式設計練習，測試你對各種概念的理解，讓你的程式設計能力更上一層樓。

質因數

質因數

計算指定自然數的質因數。

畢氏三元組

畢氏三元組

給定整數 N，找出所有滿足 a + b + c = N 的畢氏三元組。

倍數之和

倍數之和

給定一個數字，求出指定數字的所有倍數之和，範圍到該數字為止但不含該數字。

查看 Exercism 上所有 Lean 練習

Lean 的核心功能

Lean

純函式

確定性的函式讓程式碼可預測、可組合，也更容易理解。

依值型別

把規則直接編碼進型別，能讓型別自我說明，也讓無效的狀態無從表示。

程式與證明

用同一種語言撰寫程式並證明其正確性。規格就是程式碼。

經證明的正確性

用數學證明程式碼的關鍵性質，超越測試所能做到的範圍。

型別類別

將型別歸入類別，能提供輕量且可擴充的抽象。

強大的中繼程式設計

強大的巨集與 elaborator 框架，讓你擴充語言以符合自己的領域需求。

以 Lean 的方式獲得引導

每種語言都有自己做事的方式。Lean 也不例外。我們的導師會幫助你學會像 Lean 開發者那樣思考，以及如何寫出 道地的 Lean 程式碼。解完一個練習後，把它提交給我們的 志工團隊，他們會給你提示、想法和回饋，告訴你 怎麼寫得更像你在 Lean 中平常會看到的樣子。他們也會幫助你發現那些 你不知道自己不知道的事。

進一步了解引導

由社群提供的 Lean 練習

Exercism 上的 Lean 學習軌道有 100 個練習，幫助你寫出更好的程式碼。

查看所有 Lean 練習
Lean

開始使用 Lean 學習軌道

最棒的是，它對所有人 100% 免費。

加入 Lean 學習軌道