Agda でのプログラミング

Agda は証明は得意なんだけど、プログラミングはどうなの? なんですが、

　　まぁ、Haskell と同じ

なので、普通に関数を定義して、

　　C-C C-N で、eval る

eval のがおまけなのが Agda っぽい。ただ、

　　型システムが違うので、Haskell で動かしてからでも、結構、エラーがでる

暗黙の引数を含めて、適当に与えないと評価してくれないのが... でも、まぁ、なんとかなりそうです。

いや、Agda のプログラミング楽しいよ。