今日のCoq

午前中時間が空いた。

Inductive ok_day : day -> Prop :=
 | okd_gd : forall d:day,
    good_day d -> ok_day d
 | okd_before : forall d1 d2 : day,
    ok_day d2 -> day_before d2 d1 ->
    ok_day d1.

という型定義において、

okd_gd は（コンストラクタ）関数である
good_day d という命題を引数に取り、
od_day dという命題を返す

命題によるプログラミングの章にさらっと書かれていた

 命題（パラメータ化された命題も含む）はCoqにおける第一級（first-class）市民です。 このため、ほかの定義の中でこれらの命題を使うことができます。 

というのは、そのことなんだろう。
使う。というのが理解出来ていなかった。

その上でなお、書き方に対する疑問は残る。

Definition gdsa : good_day saturday :=
 gd_sat.

上記にように書けることからも、gd_satは 「good_day saturday」という命題を生み出すコンストラクタであるのは分かる。

なんで、

Definition okdsaturday : ok_day saturday :=
 okd_gd saturday gd_sat.

okd_gdの後に、saturdayとか書かんとあかんの？

多相的なlistの定義の

Inductive list (X:Type) : Type :=
  | nil : list X
  | cons : X → list X → list X.

(X:Type) が(forall X:Type)みたいな感じか？
いまいちまだ納得出来てないけど、先に進もう。