プログラミング言語や証明支援系において、既存の型を組み合わせるのではなくて、まったく新しい型（値の集合）を定義する場合は、帰納的型〈inductive type〉として定義することになります。帰納的型の上の関数は、帰納的に定義できます。このことを帰納原…