問題タブ [coinduction]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
41 問題
0
投票する
1
に答える
161
参照
coq - 余自然数の帰納法の証明
私は造語があまり得意ではないことを認めなければなりません。共自然数の二重シミュレーションの原理を示そうとしていますが、(対称) ケースのペアで立ち往生しています。
これは、最初に認められたケースに焦点を当てたときのコンテキストがどのように見えるかです。
考え？
0
投票する
1
に答える
193
参照
proof - CoNat : 0 が左に中立であることを証明する
Jesper Cockx と Andreas Abel によるこの論文CoNatから引用した の定義を試しています。
私は定義zeroし、plus：
そして、私は二相似性を定義します:
しかし、私は と似ている証明に行き詰まっていplus zero nますn。私の推測では、証明には (少なくとも) with-clause for が必要ですiszero n:
しかし、Agda は次のエラー メッセージに対して不平を言っています。
この証明はどうすればできますか？