Lean 4 極簡教學 (Using VS Code on macOS)

 1. Install Lean Environment:
https://lean-lang.org/install/

試著完Step one, two, three

2. 在VS code下，建一新的project:
取名Hello_World

3. 嘗試執行Main.lean:

一開始：

fit0721@FIT0721deMacBook-Pro Hello_World % lean --run Main.lean

Main.lean:1:0: error: unknown module prefix 'HelloWorld'

No directory 'HelloWorld' or file 'HelloWorld.olean' in the search path entries:

/Users/fit0721/.elan/toolchains/leanprover--lean4---v4.34.0/lib/lean

之後將lean --run Main.lean, 改成

lake build

lake env lean --run Main.lean

:

fit0721@FIT0721deMacBook-Pro Hello_World % lake build

lake env lean --run Main.lean

Build completed successfully (8 jobs).

Hello, world!

lake env 的意思是：先載入目前 Lean 專案的 Lake 環境，再執行後面的命令。

所以：

lake env lean --run Main.lean

可以拆成：

lake env   lean --run Main.lean
^^^^^^^^   ^^^^^^^^^^^^^^^^^^^^
設定專案環境     真正執行 Lean

lake env 會幫你把目前專案的套件、.olean 模組搜尋路徑、Lean toolchain 等環境設定好。

4. 嘗試加入一個新的定理，在Main.lean改寫如下：

import HelloWorld

def main : IO Unit :=

IO.println s!"Hello, {hello}!"

def double (n : Nat) : Nat :=

n + n

theorem double_ge (n : Nat) : n ≤ double n := by

unfold double

exact Nat.le_add_right n n

以上可以正常build，只是執行時，還是只會print Hello, world!

這邊可以小玩一下，故意改成錯的：

import HelloWorld

def main : IO Unit :=

IO.println s!"Hello, {hello}!"

def double (n : Nat) : Nat :=

n + n

theorem double_ge (n : Nat) : n + n + n ≤ double n := by

unfold double

exact Nat.le_add_right n n

就會顯示：

注意11行，會有錯誤叉叉。

Note: 

≤ 在Lean4中打 \le 再按空白鍵

類似的常用符號還有：\ge → ≥、\ne → ≠、\and → ∧、\or → ∨、\to → →、\forall → ∀、\exists → ∃。