在 Lean 軌道上測試

執行測試

執行測試之前，請先確認已安裝 Lean 4。

在練習目錄中執行：

lake test

解題

練習的解答是一個 Lean 模組。 模組的名稱定義在測試套件開頭的_匯入敘述_中：

import LeanTest
import ExerciseName

open LeanTest

def exerciseNameTests : TestSuite :=
  (TestSuite.empty "ExerciseName")
  |>.addTest "first test" (do
        return assertEqual someVal (ExerciseName.someFun someArg1 someArg2))
    ...

def main : IO UInt32 := do
  runTestSuitesWithExitCode [exerciseNameTests]

在這個例子中，測試檔在第 2 行匯入了一個名為 ExerciseName 的模組。 測試 first test 會呼叫函式 ExerciseName.someFun，並傳入引數 someArg1 與 someArg2。 someFun 前面的這個 ExerciseName 是命名空間，定義在同名的模組裡，也就是 ExerciseName。 這表示你必須建立一個名為 ExerciseName.lean 的檔案，內容就像這樣：

namespace ExerciseName

def someFun (someArg1 : Type1) (someArg2 : Type2) : ReturnType :=
    ...

end ExerciseName

請注意，測試通常會呼叫一或多個函式，並帶上若干引數。 這些函式都應該定義在解答模組中，且位於與模組同名的命名空間裡。

每個函式的各個引數與回傳值都有其型別。 這個型別可能是 Lean 的基本型別之一（例如 Nat、List Int 或 Option String），也可能是使用者自訂的型別。

在與測試模組相同的資料夾裡，你會找到一個名稱正確的檔案。 這個檔案裡應該有一個_雛形_，包含大部分初始資訊，讓你可以把它當作解答的起點。

請記得，這個雛形只是為了讓你起步。 如果你覺得有更好的做法，儘管把它整個改掉。

使用套件

使用 Lake 的 Lean 專案隨時都可以匯入標準函式庫 Std，它包含了額外的資料結構、I/O 與系統 API，以及其他基本工具。 這個匯入應該放在檔案的開頭：

import Std

def someMap : Std.HashMap Int Nat := ...

在這個例子中，型別 HashMap 以 Std 來限定，也就是定義它的命名空間。 標準函式庫中的所有資源都位於同一個命名空間 Std。

你也可以開啟一個模組，讓它所有的資料結構與函式不需要加上命名空間限定就能使用：

import Std

open Std

def someSet : TreeSet String := ...

外部套件無法直接使用，必須在 lakefile.toml 中將其加入為相依項目。

在本機開發時，你可以使用任何你喜歡的套件。 不過，線上測試執行器只能取用標準函式庫 Std。