初めての投稿です、間違っていたらすみません。
Coq では、Stream のような帰納的型には決定可能な等価性がないのではないかと思います。つまり、2 つのストリーム s と t が与えられた場合、s=t か ~(s=t) かを識別することはできません。これは、Coq のすべての導帰型に当てはまると思います。
スタック交換による簡単なグーグル検索と検索では、確認は得られません。誰かがこれを確認したり、私を修正したりできますか?
初めての投稿です、間違っていたらすみません。
Coq では、Stream のような帰納的型には決定可能な等価性がないのではないかと思います。つまり、2 つのストリーム s と t が与えられた場合、s=t か ~(s=t) かを識別することはできません。これは、Coq のすべての導帰型に当てはまると思います。
スタック交換による簡単なグーグル検索と検索では、確認は得られません。誰かがこれを確認したり、私を修正したりできますか?