Lean
Microsoft Research 製の Theorem Prover / Programming Language
Lean4 で結構いろいろ変わったぽい
web にあるチュートリアルは Lean 2, Lean 3 のものが多いので注意
Hello world
code:lean
def main : IO Unit := IO.println "Hello, world!"
Hello theorem
code:lean
theorem ex0 : p → p := by
intro h
assumption
インストール
elan というバージョンマネージャーで入れるのが便利そう code:sh
brew install elan
elan で最新の Lean を入れる
code:sh
elan default leanprover/lean4:stable
これで lean と leanpkg が install される。leanpkg は npm 的なものっぽい。
code:sh
leanpkg init proj-name
でカレントディレクトリに proj-name パッケージの boilerplate が展開される。(git init もされる)。かなりモダンな作りになっている印象