2012年11月09日
終わらない～
- 2012-11-09 (Fri)
- 一般
たかが結合則と分配則ごときを１日かけても証明できないとは…… なるべくプログラムの等式変換で証明しようとしているから面倒なのかね．うまい具合に述語を定義してやれば結構簡単にきそうな気配だけど．
閑話休題．
広いセミナー室に二人ほぼ会話なしで６時間ぶっ続けて証明を書き続けるとかいうことをしても敵は依然として大きいまま．Leibniz equality でなく任意の同値関係を使えるように定式化しようとすると色々な既存の資源が使えなくなるので面倒この上ない．少なくとも Proper のインスタンスを大量に用意せんと身動き取れないし．
閑話休題．
さて，帰り支度をするか．
- Comments: 0
- TrackBack (Close): -