今日のCoq

やはり先週詰ってたとこで詰まる。

全称記号つき命題を特定の値を伴って関数に渡したりする場合がよくわかっておりません。

Inductive ev :nat  -> Prop :=
 | ev_O : ev O
 | ev_SS : forall n : nat, ev n -> ev (S (S n)).

で、コンストラクタ関数 ev_SSに何が渡せるか。
特定の値（例えば 2とか0とか名前のついた変数とか）はそのまま渡せる・・・らしい

ev_SS 2 (ev 2) ---- ev (S (S 2))
（fun (n:nat) => ev_SS n (ev n)） ~ ev (S (S n))

この辺は習うより慣れろっぽい。ざっと読んで問題解くのを繰り返すしかないようだが。

もちろん面倒くさい。

---

ベランダの鳩は、抱卵放棄した様子。
やっぱ無理だったか。

C-x C-v 開き直す