Coqで高精度計算サイト 高精度計算サイトというのを見つけた。ここの電卓サービスは素晴らしく、大変感銘したのだが、一つ残念な点があった。 それは大きな数を扱うことができないということである。 例えば10^10000000のような大変大きな計算を実行すると答…

CoqではExtractionという機能があるためにOCamlやHaskellなどの関数型言語との連携が容易である。 CoqでOCamlの型や関数を使いたい場合は単に関数の引数として渡せば良いだけだからである。 ただ、沢山の型や関数を一度に渡したい場合、結構面倒である。Coq…