型 、型関数、構成子(コンストラクタ)
Inductive myprod (X Y : Type) : Type := mypair : X -> Y -> myprod X Y. Check myprod. (* <- 型を生む関数 *) Check myprod nat nat. (* <- (型関数 myprod が型引数 nat natを取って出来た)型 *) Check mypair nat bool 1 false. (* 構成子 mypairによって生成された、myprod nat bool 型の値。 *)
暗黙の型宣言をしていない場合は、型引数を型関数も構成子も取る必要がある。
単なる言語仕様でもあるので覚える必要あり。
型を生むのも関数であったり、なんでも関数なところは、多分他の関数型言語も同じに違いない。慣れるべし。