型推論は、型を推論するものである。多相的な型の型パラメータの値は、推論される型じゃないので省略出来ない。 Inductive list (X:Type) : Type := | nil : list X | cons : X -> list X -> list X.の Xみたいなやつね。型パラメータを持つ多相的な型のコン…

Lists.v 自分で問題を考えましょう。 - [cons] （[::]）、 [snoc]、 [append] （[++]） に関する、自明でない定理を考えて書きなさい。 とかいう問題が一番なにしたらいいか分からない。 定理ってどうやって思い付けばいいの？ Lemma nil_rev : forall l : n…

関数を宣言するときに型パラメータを暗黙に指定させてしまうことも出来るようだ。 Fixpoint length {X:Type} (l:list X) : nat := match l with | nil => 0 | cons h t => S (length'' t) end.{X:Type}のように中括弧で宣言すると型パラメータは実際に書かな…