Coq + Proof Generalで使うキーシーケンス

  • 6
    いいね
  • 0
    コメント
この記事は最終更新日から1年以上が経過しています。

基本的なものから。覚え方にあるキーワードはemacsの関数名からの推測です。
検証はCoq 8.4、Proof General 4.3で行いました。

キーシーケンス

ヘルプ

機能 キー 覚え方
キーシーケンスと関数の対応表を表示 C-c C-h Help

基本

機能 キー 覚え方
次のコマンドを実行 C-c C-n Next
前のコマンド実行を巻き戻す C-c C-u Undo
バッファの最後まで実行 C-c C-b Buffer
バッファの先頭まで巻き戻す C-c C-r Retract
カーソル位置のコマンドまで実行 C-c C-RET
SearchAbout1 C-c C-a C-a

スクリプト処理

機能 キー 覚え方
前のコマンド実行を巻き戻して、コードを削除 C-c BS
.を打った時に自動でC-c C-n(トグル) C-c . コマンドの終端.

編集

機能 キー 覚え方
実行済み部分の次へカーソルを移動 C-c C-.
introsを自動挿入 C-c C-a C-i Intros
型に対してmatchを自動生成 C-c C-a RET
タクティックの補完入力 C-c C-a C-t Tactic

証明補助

機能 キー 覚え方
既存の証明・定義を一覧表示 C-c C-t conText?
About C-c C-a C-b
Check C-c C-a C-c Check
SearchPattern C-c C-a C-o
Print Hint C-c C-a h Hint
Print C-c C-a C-p Print
i番目のゴールを表示 C-c C-a C-s
現在の*goal*バッファの内容を凍結して表示 C-c C-a g Goal
現在の*response*バッファの内容を凍結して表示 C-c C-a r Response

見た目の制御

機能 キー 覚え方
*goal*バッファの表示 C-c C-i
設定されたウィンドウレイアウトを復帰 C-c C-l Layout
バッファのローテーションを行う C-c C-o
*response*バッファをクリア C-c C-w
ツールバーを表示 / 非表示 C-c b toolBar?
カーソル位置の証明・定義を展開 / 折り畳み C-c v Visibility

プロセスの制御

機能 キー 覚え方
Coqプロセスを開始 C-c C-s Start
Coqプロセスを終了 C-c C-x eXit
スクリプト処理の中断 C-c C-c Cancel

参考になるドキュメント

*Help* (C-c C-h)
Vernacular Commands Index


  1. SearchAboutはCoq8.5以降ではdeprecatedで、Searchと呼ばれるようになったようです。