Tool. agda 的開發工具 [agda-0001]

我使用的編輯器工具是 Agda Mode on VS Code，也可以用 emacs 之類的。常用操作有

• ctrl+c, ctrl+l 會編譯檢查檔案，假設程式中有 ?，會被替換成所謂的 hole {! !}，其實就是待寫的程式

• ctrl+c, ctrl+, 可以窺看 hole 的目標類型，與當前 context 有哪些 term 可用

• ctrl+c, ctrl+r 會把 hole 中你打的程式碼往前提取，當然前提是類型是正確的

• ctrl+c, ctrl+m 會把 hole 中你打的程式碼直接當成結果，一樣類型要是正確的

• 一般來說一個 agda 定義如下

  hello : A → B
  hello a = {! !}

  ctrl+c, ctrl+c 會問你要把哪個變數用構造子分開，回答 a，假設有 a1 與 a2 兩個構造子，程式就會變成

  hello : A → B
  hello a1 = {! !}
  hello a2 = {! !}

使用 Linux 的使用者可以更改預設的 copy/cut 指令以免衝突。