Coq クィックリファレンス

Coq クィックリファレンス 書きかけだけれど、たぶん永遠に書きかけなので、とりあえず書いたところだけ公開。 基礎知識 Gallina の構文と Vernacular コマンド オプション モジュール Prop vs. Set vs. Type タクティク リファレンス 証明の補助: idtac, fail, move, clear, set, remember, pose, rename, intro, assert, cut, lapply, specialize, generalize 項による証明: exact, refine, apply コンストラクタの適用: constructor, split, exists, left, right 否定と矛盾: absurd, contradict, contradiction, exfalso 帰納法と場合分け: fix, cofix