memo

Coq演習

課題12 難しすぎ。

先人のを参考に丸写し。あとで見直す。

あらためて読んで、代数的データ型というものをちっとも分かっていなかった。
existsもforallに似てるけど、TrueやFalseや果てはnatやlistのお仲間(代数的データ型)に過ぎないということ。

あと、証明木に慣れたい。