はじめに 昨日、スタート Ssreflect というイベントに参加して、Coq + ssreflect のハンズオン的なものをやりました。 Coq 環境といえば、Emacs の ProofGeneral が非常に有名です。 しかし、私は Emacs は終了の仕方すら分からないレベルの初心者なので Emacs + ProofGeneral ではチュートリアルの例題を打ち込むだけでも非常に苦労しました。 証明も普段使い慣れている Vim で何とかできないかと思い調べたところ、そこそこ良さ気な環境を構築できたので紹介します。 使用するプラグイン 以下の2つをインストールします。NeoBundle のようなパッケージマネージャを使用するのをおすすめします。 jvoorhis/coq.vim vim-scripts/CoqIDE jvoorhis/coq.vim は Coq のシンタックスとインデン