Leanセットアップ方法メモ 2025/6/28

やってみようという気分が再燃してきた. 個人メモ

現在は Lean4

ツール一覧

elan

elan は、rustup や ghcup と同様に、Lean のツールチェーンを管理します。

lake

lake は、cargo・make・Gradle と同様に、Lean パッケージとその依存関係をビルドします。

lean

lean（シェルコマンド）は、個々の Lean ファイルを型検査し、コンパイルするだけでなく、編集中のファイルに関する情報をプログラマツールに提供します。通常、lean はユーザが直接呼び出すのではなく、他のツールによって呼び出されます。

公式のセットアップページがある

Supported Platforms の Tier 表もここ

ターミナル上でセットアップする方法でやる

curl https://elan.lean-lang.org/elan-init.sh -sSf | sh

vscode 経由よりもこっちでやりたかった

PATHを通す

elan が使えるようになる

elan --version

lake と lean に PATH が通った状態になる

Lake version 5.0.0-b02228b (Lean version 4.20.0)

初回実行時にダウンロードが走った

Lean (version 4.20.0, arm64-apple-darwin23.6.0, commit b02228b03f65, Release)

動作確認

lean --run <(echo '#eval 2 + 3')

REPL なさそう

FizzBuzz

code:sh

echo 'def fizzbuzz (n : Nat) : String :=

match n % 15, n % 3, n % 5 with

| 0, _, _ => "FizzBuzz"

| _, 0, _ => "Fizz"

| _, _, 0 => "Buzz"

| _, _, _ => toString n

code:sh

echo 'def fizzbuzz (n : Nat) : String :=

if 15 ∣ n then "FizzBuzz"

else if 3 ∣ n then "Fizz"

else if 5 ∣ n then "Buzz"

else toString n

code:sh

echo 'inductive FizzBuzzResult

| fizz | buzz | fizzbuzz | number (n : Nat)

def classify (n : Nat) : FizzBuzzResult :=

if n % 15 = 0 then .fizzbuzz

else if n % 3 = 0 then .fizz

else if n % 5 = 0 then .buzz

else .number n

def fizzbuzz (n : Nat) : String :=

match classify n with

| .fizz => "Fizz"

| .buzz => "Buzz"

| .fizzbuzz => "FizzBuzz"

| .number n => toString n