どうやら Agda2 はまだ主流じゃない(?)ような感じなので、まずは Agda1 を触ってみようと思った。こっちならチュートリアルとかも少しはあるし。というかそもそもの動機の論文では Agda1 を使ってるし…。(最初に気づいとけよ)

Agda2 まじわかんない。心折れそう。とりあえず agda-mode で使い方がわかったやつを適当 メモ。そのうち追加します。 C-c C-x C-l agda で証明を開始。 ? 証明がよくわからないところは ? で埋める。 assoc x y z = ? これで C-c C-x C-l とすると ? がゴー…