参考は http://www.cs.chalmers.se/~ulfn/darcs/AFP08/LectureNotes/AgdaIntro.pdf とAgda2添付のexamples、そしてソースコード。一応emacsインタフェースで、コード補完(別名、証明補助)できるUIがあるのですが、自分はまったく使ってません。一応、こうい…