Type，Prop，Sort¶
まず，型そのものがどの階層に住んでいるかを整理します．
この節で扱う Type，Prop，Sort は「型の構成方法」ではなく，「型がどの階層にあるか」を表す語です．
Type は通常のデータ型が住む階層です．
たとえば Nat : Type，Int : Type，List Nat : Type です．
また Type 自身にも型があり，Type : Type 1 です．
Type : Type としてしまうと自己言及的な循環が起きるため，Lean では Type 0 : Type 1，Type 1 : Type 2，... という階層を使います．
Prop は命題が住む階層です．
P : Prop の項は，命題 P の証明です．
Sort は Prop と Type u をまとめて扱うためのより一般的な階層で，おおまかに Sort 0 が Prop，Sort (u + 1) が Type u に対応します．
#check Prop
#check Type
#check Type 1
#check Sort 0
#check Sort 1
universe u v
def sampleNumber : Nat := 42
def sampleList : List Nat := [1, 2, 3]
example : sampleList.length = 3 := by
rfl
def idSort (α : Sort u) (x : α) : α :=
x
example : idSort Nat 7 = 7 := by
rfl
example (P : Prop) (h : P) : idSort P h = h := by
rfl
def idType (α : Type u) (x : α) : α :=
x
example : idType Nat 5 = 5 := by
rfl
example : idType (List Nat) [1, 2] = [1, 2] := by
rfl
idSort は Prop と Type の両方に使えます．
一方，通常の数学的対象を引数に取る関数では α : Type u と書くことが多いです．
この章では universe 変数を明示していますが，Lean が自動的に universe を推論してくれる場面も多くあります．
演習¶
#check で次の式の型を確認してください．