Coqの中で定義したり証明の対象にした関数を、ふと日常生活で使いたくなるときがある。 そんなときはExtractionコマンドが大変便利である。 文法 [Extraction 関数名] 例えば次のような恒等関数を作ってExtractionしてみる Coq Definition id (A:Set)(x:A) :…

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