2007-06-17から1日間の記事一覧

Coqの世界から現実世界へ

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

Coqで作った関数を実生活で使用する