問題タブ [coq-tactic]
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.
356 問題
0
投票する
0
に答える
431
参照
coq - Ltac : forall 仮説をインスタンス化する
私は2つの新しい仮説を作成する戦術に取り組んでいます
その形の仮説から
これが私のLtacコードです：
was はh、分解する仮説x、新しい変数tの名前、および新しい仮説の名前です。戦術は意図したとおりに機能しますが、証明の最後に次のようになります。
このevar戦術は、既存のタイプを使用する代わりに、D という名前の新しいタイプを作成したようです。私が使用する場合は注意してください
代わりにcoqtopでは完全に機能します。
0
投票する
1
に答える
161
参照
coq - 余自然数の帰納法の証明
私は造語があまり得意ではないことを認めなければなりません。共自然数の二重シミュレーションの原理を示そうとしていますが、(対称) ケースのペアで立ち往生しています。
これは、最初に認められたケースに焦点を当てたときのコンテキストがどのように見えるかです。
考え？