Binary Tree

いや、いつもの Model 検査を Agda で書いてるんですが、

　　Binary Tree が無限ループする

まぁ、それ自体はよくあるバグなんですが、

　　それって正しいのを証明したやつじゃなかった?

ん〜 まぁ、それもありがちなんだが。そもそも、

　　Haskell / Agda って bug った時の debug 方法があんまりない

コードを分解して実行するくらい。trace とかあるらしいんだけど...

で、test code を動かしてたら、

　　なんか -- wrong とか書いてある。は?

う、そういえば、

　　元のコードに bug を入れておく方が面白い

と思ってそのままにしたのだった。証明入れたコードとは別なのかよ。いや、

　　自分で書いたんですけどね

で、どうするの。なおすか、証明付きの方を使うか... それも面白いといえば面白いか。