■

関数を宣言するときに型パラメータを暗黙に指定させてしまうことも出来るようだ。

Fixpoint length {X:Type} (l:list X) : nat :=
  match l with
  | nil => 0
  | cons h t => S (length'' t)
  end.

{X:Type}のように中括弧で宣言すると型パラメータは実際に書かなくてよくなる。

Eval simpl in length [1;2;3].
= 3 : nat

*

そして対象とメタがごちゃごちゃになって、訳分からんくなり果てる。
ポインタのときもそうだった気がする。
何を指しているか？
何が指しているか？
どれがポインタ変数で、ポインタが指しているものは何か？

多相的な型で変更出来る型はどうやって渡すか？ その型の値はどこで渡すか？

このへんのことは、HaskellとかOcamlとかやってたら分かるようになってたのかねえ？
いきなりCoqに手を出したのは失敗だったかもしらん。