example

example は名前を付けずに命題の証明をすることができるコマンドです。

より正確には、example : T := t は t が型 T を持っていることを確かめます。特に T の型が Prop であるときには、最初に述べた通り t は T の証明だとみなすことができます。

-- `1 + 1 = 2` は `rfl` で証明できる
example : 1 + 1 = 2 := rfl

-- `rfl` という項の型が `1 + 1 = 2` であると言っても同じこと
#check (rfl : 1 + 1 = 2)

-- `n + 0 = n` は `rfl` で証明できる
example {n : Nat} : n + 0 = n := rfl

-- `{n : Nat} → n + 0 = n` という依存関数型の項を `rfl` で構成できる、と言い換えられる
#check (rfl : {n : Nat} → n + 0 = n)

-- `[1, 2, 3]` は `List Nat` 型の項
example : List Nat := [1, 2, 3]

-- `#[1, 2, 3]` は `Array Nat` 型の項
example : Array Nat := #[1, 2, 3]

-- `true` は `Bool` 型の項
example : Bool := true