問題タブ [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.

0 投票する
3 に答える
689 参照

coq - Coq に括弧を出力させることはできますか?

私はCoqを初めて使用し、集合論的証明の作成に取り組んでいます。

括弧が省略されていて、式が読みにくいことに気付きました。例えば、

しかし、Coqに印刷してもらいたい(A :\: A) :|: (A :&: B) = Bです。上記の出力は、次のコードによって得られます。

setDDr驚いたことに、finset.vの元のコーディングを見ると、次のように括弧が付いています。

だから私はなぜ括弧が消えるのか、どのように Coq に CoqIde で括弧を明示的に出力させるのか疑問に思っています。

0 投票する
1 に答える
456 参照

keyboard - Coqide キーバインドのバグ(?)

少し奇妙な問題が発生しています...最近、CoqIDE を使用しているときにいくつかの奇妙な状況が発生しています。

  1. windows/superキーを押さないと文字「v」を入力できません。

  2. 複数のウィンドウが開いている場合、バックスペースを押すとフォーカスが前のタブに移動します。それで物事を削除することはできません。ただし、チャンクの削除には CTRL+backspace が機能します。

キーマップを US から GB に変更した後に最初の 2 つ (発生した可能性があります) が発生しましたが、前後に切り替えても問題は解決しませんでした。

ARCH Linux を実行すると、すべてが最新の状態になり、他のアプリケーションは影響を受けません。スティッキー キーはオンになっていません。

ご提案ありがとうございます。

編集:再インストールを試みましたが、役に立ちませんでした...

解決済みの編集: ええ、あなたは完全に正しいです。気付かないうちに超高速の再バインドを行ったようです。また、.config ファイルはアプリによって生成され、マネージャーの管轄下にないため、パッケージ マネージャーは基本的に .config ファイルに触れないことも学びました。解決しました!