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では、楽しくやりがいのある演習を通して、コンセプトの理解を試しながらプログラミングを上達させられます。

言う

言う

0から999,999,999,999までの数値が与えられたら、その数値を英語で書き表します。

ローマ数字

ローマ数字

現代のアラビア数字をローマ数字に変換します。

サブリスト

サブリスト

あるリストが別のリストのサブリストかどうかを判定します。

ExercismのLean演習をすべて見る

Leanの主な機能

Lean

純粋関数型

決定的な関数は、コードを予測しやすく、組み合わせやすく、理解しやすくします。

依存型

ルールを型に直接エンコードすると、コードは自己文書化され、不正な状態は表現できなくなります。

プログラムと証明

同じ言語でプログラムを書き、その正しさを証明できます。仕様もコードです。

正しさの証明

テストだけでなく、コードの重要な性質を数学的に証明しましょう。

型クラス

型をクラスに分類することで、軽量で拡張可能な抽象化が得られます。

強力なメタプログラミング

強力なマクロとエラボレーターのフレームワークにより、自分の領域に合わせて言語を拡張できます。

Lean流のメンタリングを受ける

プログラミング言語にはそれぞれ、物事の進め方があります。Leanも 同じです。メンターが、Leanのエンジニアのように 考える方法と、Leanらしいコードの書き方を 教えてくれます。演習を解いたら、ボランティアチームに 提出してみましょう。ヒントやアイデア、フィードバックをもらい、 Leanでよく目にする書き方に近づけることができます。 自分が知らないことを知らない、ということに気づかせてくれるでしょう。

メンタリングについてもっと詳しく

コミュニティが作ったLeanの演習

ExercismのLeanトラックには、100つの演習があり、より良いコードを書くのに役立ちます。

Leanの演習をすべて見る
Lean

Leanトラックを始めましょう

何より、誰にとっても100%無料です。

Leanトラックに参加する