基本的なものから。覚え方にあるキーワードは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
