Agda のプログラミングの続き

結構順調に進んでいて、

　　assert 見たいなところに等式を書いて refl で証明!

みたいにできるんですが...

　　二分木に4個入れた所で沈黙

おい。直前に入れたものは取れるのだが、二つ前だとダメだな。

でも、refl でなければ普通に eval で値は返ってくるんですけどね。まあ、Agda にはAgdaの都合があるんでしょう。

昨日はもつ鍋でしたが、さすがにテンパってるM2は釣れないか。いや、来てくれた人も。