- 2012-10-22 (Mon) 23:11
- 一般
Proof General で Compile Before Require のオプションを使っているのだけど，たまには rm *.vo *.glob してやったほうが良いのかもしれない．とりあえず意味不明な挙動が解消された気がする．……気がするだけかもしれない．
つか，Proof. typeclasses eauto. Qed. で証明できるのに証明が必要とかわけわからん．いまひとつ typeclass のリゾルバの挙動がつかめん．Implicit arguments の決定とのタイミングとかが問題なのか？
- Newer: ことはじめ