Seeker's eye

Wednesday, 3 December 2025

Lean 4

Agda と同じ定理証明系なんですが、少し触ってみようかと

VSCode で入れるらしいが、入るけど

　　なに入力すればいいの?

まぁ、ChatGTPに聞けばいいか。#eval 1 + 2 とかするらしい

import First.Basic

#eval 1 + 2

def square (x : Nat) : Nat :=
x * x

#eval square 4

theorem hello1 : 1 + 1 = 2 := by
decide

コマンドラインからできるんだろと思ったが、なんか、動かない

+leo+kono ~/.elan/bin/lean First.lean
First.lean:3:0: error: unknown module prefix 'First'
No directory 'First' or file 'First.olean' in the search path entries:

build は動く

+leo+kono ~/.elan/bin/lake build -v First.lean
ℹ [2/3] Replayed First.Basic
trace: .> LEAN_PATH=/Users/kono/src/lean/test1/First/.lake/build/lib/lean /Users/kono/.elan/toolchains/leanprover--lean4---v4.25.2/bin/lean /Users/kono/src/lean/test1/First/First/Basic.lean -o /Users/kono/src/lean/test1/First/.lake/build/lib/lean/First/Basic.olean -i /Users/kono/src/lean/test1/First/.lake/build/lib/lean/First/Basic.ilean -c /Users/kono/src/lean/test1/First/.lake/build/ir/First/Basic.c --setup /Users/kono/src/lean/test1/First/.lake/build/ir/First/Basic.setup.json --json
ℹ [3/3] Replayed First
trace: .> LEAN_PATH=/Users/kono/src/lean/test1/First/.lake/build/lib/lean /Users/kono/.elan/toolchains/leanprover--lean4---v4.25.2/bin/lean /Users/kono/src/lean/test1/First/First.lean -o /Users/kono/src/lean/test1/First/.lake/build/lib/lean/First.olean -i /Users/kono/src/lean/test1/First/.lake/build/lib/lean/First.ilean -c /Users/kono/src/lean/test1/First/.lake/build/ir/First.c --setup /Users/kono/src/lean/test1/First/.lake/build/ir/First.setup.json --json
info: First.lean:5:0: 3
info: First.lean:10:0: 16
Build completed successfully (3 jobs).

なんか、結構、えげつない呼び出しだな

まぁ、動いたみたい。

一旦、C に変換するの? 微妙だな

agda みたいに「全部、Haskell でがんばる」ってのがいいかどうかは、また別だけどね