2014-11-21から1日間の記事一覧

Coq入門 - 3

coq

Coq入門 - 2.1 - エンジニアですよ! に追記したが、Lemma le_n_0_eqが証明できた あと補完が効くようになったらなぜか.を押すだけでC-c C-n相当の部分まで進むようになった。 False_indやFalseの証明の仕方が少しわかった。 しかし、その後も証明ははかどら…