Edited at

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

More than 1 year has passed since last update.

基本的なものから。覚え方にあるキーワードは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と呼ばれるようになったようです。