- 2012-11-02 (Fri) 23:44
- 一般
証明というか項というか，その構成途中に展開できないものを使ってしまうと Eval で評価して動作確認ができなくなる．んで，どの場所が展開不能なのか探り当ててそれを使わない方向で証明を書きなおし…… とかいう作業がちらほら．XX_dec 系のは動くプログラムとして使いたいけど直接プログラム書くのが面倒だから証明しちゃえとかやるとこうなる．
折衷案としては危なそうな部分は手で書いておいて細かい部分を個々に証明して埋めるってのかね．
- Newer: ことはじめ