問題タブ [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
投票する
1
に答える
59
参照
coq - ローカル コンテキストから仮定を自動的に選択する
次のようなセクションを持つ証明スクリプトがあります。
きれいに解決するために使用するための選択候補のようですが;、残念ながら仮説はいたるところにあります。さまざまなサブプルーフを一緒に折りたたむにはどうすればよいですか?
0
投票する
2
に答える
375
参照
coq - Ltac パターン マッチング: なぜ「forall x, ?P x」は「forall x, x」と一致しないのですか?
私は素朴に成功することを期待checkForall Hしますが、そうではありません。
Adam Chlipalaは、彼の著書Certified Programming with Dependent Typesで、依存型に対するパターン マッチングの制限について説明しています。
問題は、統合変数にローカルにバインドされた変数が含まれていない可能性があることです。
これが私がここで見ている動作の理由ですか?