Lean 4 code generation best practices. Use when writing Lean 4 code to avoid common AI mistakes with syntax, types, tactics, and project configuration.
AI が Lean 4 コードを生成する際のベストプラクティス。
lake new myproject # 新規プロジェクト作成
lake build # ビルド
lake env printPaths # 検索パス表示
lakefile の設定は reference/configuration.md を参照。
#check Nat.add -- 型シグネチャを表示
#eval 2 + 3 -- 式を評価
#print Nat.add -- 定義を表示
#check @List.map -- 暗黙引数を含む型を表示
ツール詳細は reference/ide.md を参照。
do, where, match, if でインデントが重要:= を使う（= ではない） - def f (x : Nat) : Nat := x + 1by でタクティックモードに入る - theorem t : P := by exact h（by なしは不可）Type は Type 0、Type 1 は Type 0 を含むsorry は未完成の穴 - コンパイルは通るが証明未完了（本番コードに残さない）#eval で Prop は評価できない - #check か Decidable インスタンスを使う{} とインスタンス [] - [] は型クラス解決を起動するmatch には with が必要 - match x with | ...（with なしはエラー）if には then/else が両方必要 - else なしの if-then は不可decreasing_by や termination_by を使う-- NG: `:=` がない
def double (n : Nat) : Nat
n + n
-- OK
def double (n : Nat) : Nat :=
n + n
-- OK: 等式コンパイラスタイル（パターンマッチ）
def double : Nat -> Nat
| n => n + n
-- NG: `with` がない
def isZero (n : Nat) : Bool :=
match n
| 0 => true
| _ => false
-- OK
def isZero (n : Nat) : Bool :=
match n with
| 0 => true
| _ => false
-- NG: `do` キーワードがない
def main : IO Unit :=
IO.println "hello"
IO.println "world"
-- OK
def main : IO Unit := do
IO.println "hello"
IO.println "world"
-- NG: 命題の証明に `def` を使っている
def myTheorem : 1 + 1 = 2 := by rfl
-- OK: 命題には `theorem` を使う（実行時に消去される）
theorem myTheorem : 1 + 1 = 2 := by rfl
-- NG: 他言語風の `{` `}`
structure Point {
x : Float
y : Float
}
-- OK: `where` 構文を使う
structure Point where
x : Float
y : Float
-- NG: モナディックバインドに `let x = ...` を使っている
def readAndPrint : IO Unit := do
let line = IO.getStdIn >>= fun stdin => stdin.getLine
-- OK: モナディックバインドには `<-` を使う
def readAndPrint : IO Unit := do
let stdin <- IO.getStdin
let line <- stdin.getLine
IO.println line
| 項目 | コマンド / 構文 | 説明 |
|---|---|---|
| ビルド | lake build | プロジェクトをビルド |
| 実行 | lake env lean --run Main.lean | main を実行 |
| REPL | lake env lean | 対話モード |
| 型チェック | #check expr | 型を表示 |
| 評価 | #eval expr | 式を評価 |
| 定義表示 | #print name | 定義を表示 |
| 検索 | exact? / apply? | タクティック・補題を検索 |
| ドキュメント | https://leanprover-community.github.io/mathlib4_docs/ | Mathlib ドキュメント |
各トピックの詳細は以下のファイルを参照:
| ファイル | 内容 |
|---|---|
| reference/language.md | 型、構文、パターンマッチ、型クラス、モナド、do 記法 |
| reference/tactics.md | タクティック: intro, apply, exact, simp, omega, rw, induction 等 |
| reference/stdlib.md | 標準ライブラリ、Batteries、Mathlib 基礎、よく使う型 |
| reference/configuration.md | lakefile.toml, lean-toolchain, 依存関係、プロジェクト構成 |
| reference/testing.md | #eval, #check, example, テストパターン、証明デバッグ |
| reference/ide.md | LSP 機能、Lake コマンド、エディタ連携 |