パターンマッチができるってことは、extractionできるということである。 singleton definitionのパターンマッチの場合、実は非常に簡単で、そのパターンマッチ自体が消えて、結果だけが残る。 一方、empty definitionはそうも行かない。そもそもCoqのterm上…

これが誰かの何かの役に立てば幸いなのだけれども。 さて、述語に対するパターンマッチは述語以外を返してはいけない、といった。 しかし例外がある。 それは、展開する述語がsingletonまたはempty definitionとして定義されている場合。 この場合はSetやTyp…