問題タブ [theorem]
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.
49 問題
0
投票する
3
に答える
130
参照
coq - coqで定理を証明しながら「false = true」命題に対処する方法
私はcoqが初めてで、この定理を証明しようとしています
これがイコールの定義です
これがこれまでの私の解決策です
そして、私はこのようなものになります
この出力は、定理が正しくなければならない場合、命題「偽 = 真」から命題「Var 0 = Var (S n)」が従う必要があることを意味することを理解していますが、どうすればよいかわかりません。私の証明を先に。
0
投票する
0
に答える
33
参照
types - リーンで次のエラーを解釈する方法は?
次のコードがあります。
問題は最後のステップ (ショー) にあるようです。コンパイラは次のように伝えます。
理解できません。どちらも同じタイプではないですか？