データ型
型(type)は、直観的にはデータを分類するものです。集合が要素を持つように、型は項を持つことができます。
Lean では命題 P : Prop
も型ですが、それらを除いた型は Type u
の項になります。本書では Type u
の項をデータ型と呼んでいます。
型(type)は、直観的にはデータを分類するものです。集合が要素を持つように、型は項を持つことができます。
Lean では命題 P : Prop
も型ですが、それらを除いた型は Type u
の項になります。本書では Type u
の項をデータ型と呼んでいます。