coqtop を Vim の中で動かして連携させる - EAGLE 雑記http://www.iij-ii.co.jp/lab/techdoc/coqt/ を読んでいたらいつのまにかそんなかんじのを書いていた．どうしても Vim で書きたいかわいそうな人以外は普通に CoqIDE や Proof General 使ったほうがいいと思います． https://github.com/eagletmt/coqtop-vim 最新の vimproc を先にインストールしておく必要がある． 使い方としてはまず :CoqStart で coqtop からの出力を表示するバッファとウィンドウを作る． コードを書いていき，インサートモードで するとその行まで coqtop に送られる．ノーマルモードで :CoqGoto あるいは g *1でも同じ． 既に送られた領域の最後の行は Folded で色付けされ，これより上の行は編集できなくなる． (ところで「編集できなく」するため
