More than 5 years have passed since last update.
Coq + Proof Generalで使うキーシーケンス
11
Last updated at Posted at 2016-06-08
基本的なものから。覚え方にあるキーワードは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 |
|
| 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
-
SearchAboutはCoq8.5以降ではdeprecatedで、Searchと呼ばれるようになったようです。 ↩
Register as a new user and use Qiita more conveniently
- You get articles that match your needs
- You can efficiently read back useful information
- You can use dark theme