学生の書くAgda

4年次に Agda をいじってもらっているわけですが、最近、だいぶ、まともになってきたかも。

もっとも、自分の書いたものがまともだったのかどうかも良くはわからないんですが。

自然変換が要求する等式とかを直書きしているので、natural-transformation を record で定義してくれと言ったら、

＊ record の使い方が良くわからない

とか言ってたのが1ヶ月前だったような。まぁ、僕も、そこから始めた記憶がある。でも、まだ使ってない部分があるなぁ。

なんか、作った Monadの法則の証明に10分ぐらいかかるらしい。確かに僕も、証明のチェックに時間がかかるようになってしまったことがあった。その時には、

＊　何かをやってなおした

のだけど、なんだったかなぁ。Agdaが推論を頑張らなくて良いように修正した気がするが、既に思い出せない。

Agda は、ちゃんと書くと「数学の本に書いてあるのと同じように書ける」というのがあるみたい。正しい証明の美しさ。予定調和ということか。

というわけで、修論卒論で忙しい時期です。