Meeting の合間に Agda

Agda の合間に Meeting かどうかは知りませんが、そんな感じでした。10分あると、一つ証明できるか。

証明時は難しくないことが多いけど、データ構造を決めるのが難しい感じ。あとで再利用する時に祟るし。

プログラミングと証明とは同じということだね。難しい気もするけど、基本はそれほどでもない。アセンブラに相当するのが、項書換だというだけですね。

それにしては、はまりまくることが多いけど。