2012年03月23日

補足:Falseのパターンマッチのextraction

パターンマッチができるってことは、extractionできるということである。

singleton definitionのパターンマッチの場合、実は非常に簡単で、そのパターンマッチ自体が消えて、結果だけが残る。

一方、empty definitionはそうも行かない。そもそもCoqのterm上は分岐がないのだ。

しかもFalse自体は述語なので消える運命にある。

ではどうなるのか?


結果はこれまた簡単、assert(やそれに類するもの)を使って異常状態であることを知らせる。

なぜなら、検証した結果としてはそこに来ることを想定していないわけだから。

というわけで、これでextractionも可能となり、すべてが丸く収まったわけである。


これで終わり?まだもうひとつある。でもそれはいつ書くか不明。

posted by chiguri at 00:10| Comment(0) | TrackBack(0) | Coq
この記事へのコメント
コメントを書く
お名前:

メールアドレス:

ホームページアドレス:

コメント:

この記事へのトラックバックURL
http://blog.sakura.ne.jp/tb/73554492

この記事へのトラックバック