2013-01-01から1年間の記事一覧

依存関係のある値のうちの一部をrewriteしようとしたときの問題

この記事は「Theorem Prover Advent Calendar 2013」5日目の記事である。 最近、とある大手企業のシステムのバイナリデータを扱う処理の高速化のためにCoqを使ったのだが、ちょっとアレっと思ったことを体験したのでそれを共有したいと思う。 問題の概要は表…