Agda の続き

OSC の最中にやっていた部分は順調だったんだけど、式変形を行う一種のマクロみたいなものが Agda にあるので、それを Category.agda で使えるようにしようと言う部分で、

＊　日月、二日間一歩も進まない

ってなんなの?

まぁ、そういうこともあるさ。

http://www.cr.ie.u-ryukyu.ac.jp/hg/Members/kono/Proof/category/file/2b005ec775b4/nat.agda

これの module -Reasoning ですが、誰か助けてくれるとうれしいです。とか投げてみる〜

ラグナガーデンホテルも、いよいよシーズンで、プールも、ちょっと混んできました。例年より早い感じ。やっぱり、少し景気良くなってきたみたいだね。