chiguri_s https://blog.hatena.ne.jp/chiguri_s/ chiguriの生態（嘘や誇張アリ） https://chiguri-s.hatenadiary.org/ Coq パターンマッチができるってことは、extractionできるということである。 singleton definitionのパターンマッチの場合、実は非常に簡単で、そのパターンマッチ自体が消えて、結果だけが残る。 一方、empty definitionはそうも行かない。そもそもCoqのterm上は分岐がないのだ。 しかもFalse自体は述語なので消える運命にある。 ではどうなるのか？ 結果はこれまた簡単、assert（やそれに類するもの）を使って異常状態であることを知らせる。 なぜなら、検証した結果としてはそこに来ることを想定していないわけだから。 というわけで、これでextractionも可能… 190 <iframe src="https://hatenablog-parts.com/embed?url=https%3A%2F%2Fchiguri-s.hatenadiary.org%2Fentry%2F20120323%2F1332515454" title="補足：Falseのパターンマッチのextraction - chiguriの生態（嘘や誇張アリ）" class="embed-card embed-blogcard" scrolling="no" frameborder="0" style="display: block; width: 100%; height: 190px; max-width: 500px; margin: 10px 0px;"></iframe> Hatena Blog https://hatena.blog 2012-03-23 00:10:54 rich https://chiguri-s.hatenadiary.org/entry/20120323/1332515454 1.0 100%