Coq の Program で定義した div2 を実行して時間を測ってみた。
Time Eval vm_compute in div2 1. (* 0.012 secs (0.u,0.s) *) Time Eval vm_compute in div2 2. (* 0.338 secs (0.243u,0.008s) *) Time Eval vm_compute in div2 3. (* 9.522 secs (5.68u,0.3s) *)
3 / 2 で 9秒というのはなんというか、信じ難いほど遅い。まぁ、かなり大きな証明項を作るからしょうがないのかもしれない。
[latest]