お仕事終わり

2014-07-04 (Fri) 23:33
一般

Coq のバージョンを 8.4pl2 から 8.4pl4 に上げたら今まで通っていた証明が通らなくなった．別に用意した lemma を specialize する部分で，lemma の最後の引数を与えるとエラーになるけれど，その手前で止めて specialize した後に最後の引数を与えてあげると通るとかいう意味不明な挙動で……　ちょっと typeclass を入り組んで使っているのでそのせいかもしれないなぁと思いつつ Coq をよく分かっている人に聞いてもやっぱり意味不明とのご回答．とりあえず回避策はわかったので仕事には影響ないけどバグレポートとかするにも挙動再現の最小コードを作るのが面倒そうだというのが最大の問題．

さて，シンポジウムも終わったし後は帰るだけ．

閑話休題．

Albertheijn ってスーパーは夜9時過ぎても開いてて助かった．