型 、型関数、構成子(コンストラクタ)

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 型の値。 *)

暗黙の型宣言をしていない場合は、型引数を型関数も構成子も取る必要がある。
単なる言語仕様でもあるので覚える必要あり。

型を生むのも関数であったり、なんでも関数なところは、多分他の関数型言語も同じに違いない。慣れるべし。