Agda and gitub copilot

いや、まぁ、あんまり期待してなかったんですけどね。neovim plugin で使うわけですが、

Agda って大半は自分で定義したもので、それは見てくれない。なんだが、

　　List とか Maybe なら得意だぜ

あ、そうですか。なるほどね。ただ、

　　もっともらしいが、違うものを持ってくる

のがなぁ。ChatGTP とも重なりますけどね。で、

　　え、有料なの?!

まぁ、Agda 専用なのもできるような気はするけど...