Emacs agda-mode の使い方

Agda2 まじわかんない。心折れそう。とりあえず agda-mode で使い方がわかったやつを適当　メモ。そのうち追加します。

C-c C-x C-l

agda で証明を開始。

?

証明がよくわからないところは ? で埋める。

assoc x y z = ?

これで C-c C-x C-l とすると ? がゴール(用法が正しいか不明)になる。

C-c C-c

場合分けを自動でやってくれる。

assoc x y z = {! !}

が

assoc zero y z = {! !}
assoc (suc y) y' z = {! !}

になる。