問題タブ [coqide]
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.
coq - Coq で再帰的な定義を定義できますか?
Coq では、相互に再帰的な誘導型を定義できることを知っています。しかし、Coq で再帰的な定義を記述する方法はありますか?
たとえば、定義を次のように書きたいとします。
Definition myDefinition A := forall B C, (myDefinition B) \/ (A = C).
上記の定義で重要な部分はmyDefinition Bで、別の引数で同じ定義を再帰的に呼び出しています。Coqでこれを行うことは可能ですか?
scope - Coq でのグローバル変数とローカル変数のシミュレーション
Coq でグローバル変数とローカル変数をシミュレートしようとしていますが、開始方法さえわかりません。ヒントやアドバイスをくれる人はいますか? このプログラミング言語に関するドキュメントをたくさん読みましたが、よくわかりません。前もって感謝します！
coq - Rbar / Rbar_le / コクリコ補題
Coq 8.12.0 リファレンス マニュアルで Coq を学習していますが、次の補題を証明するのに苦労しています。
そして、私は証明を終わらせるのに行き詰まります。何か案は ？