前回の記事の注意。

実は、前回書いたtype class in coqの記事、ちょっと怖いことがある。
このコードを実行すると、メモリを消費したあげくに落ちる。

Check (Compile (CEConst 1)).

もちろんEval computeやEval simplでも同様。
なぜかはよくわからないが、まともにCompileの計算ができないらしい。
証明はできているし、項の作成も必ずうまくいくことがわかっているので、正しいことは正しいはずなのだが、なぜかうまくいかない。
原因不明なので、今は近寄らないのが吉。


追記：以下のコードが通るあたり、Compileの補完がまずいようだ。

Check (let (_, c) := (CEConst 1) in c).
Check (let c := (CEConst 1) in Compile).

この補完、コードを書く上で山のように引っかかる箇所があるので、デフォルトでオンにするのをやめてほしいくらいなのだが・・・