データ型
型(type)は、直観的にはデータを分類するものです。集合が要素を持つように、型は項を持つことができます。
Lean では命題 P : Prop も型ですが、それらを除いた型は Type u の項になります。本書では Type u の項をデータ型と呼んでいます。
Press ← or → to navigate between chapters
Press S or / to search in the book
Press ? to show this help
Press Esc to hide this help
型(type)は、直観的にはデータを分類するものです。集合が要素を持つように、型は項を持つことができます。
Lean では命題 P : Prop も型ですが、それらを除いた型は Type u の項になります。本書では Type u の項をデータ型と呼んでいます。