帰納型 - mrsekut-p

帰納型

inductive types_

https://en.wikipedia.org/wiki/Inductive_type

https://ncatlab.org/nlab/show/inductive+type

帰納型 - Theorem Proving in Lean 4 日本語訳

型コンストラクタの集まりのインスタンスである

和、関数、再帰

可算無限個の宇宙

帰納型があればenumも作れるらしい

どう上位互換なのかよくわからんが