Coqは非常に疑り深いのでOCamlなどの普通のプログラミング言語の型を全然信頼しない。 このため、CoqからExtractionで引き出した関数を使う場合はCoqの型からOCamlの型への変換をしなければならないことがある。 それはint, nat, stringなどの基本的な型であ…