Wednesday, 10 January 2018

Agda でのプログラミング

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

  まぁ、Haskell と同じ

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

  C-C C-N で、eval る

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

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

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

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