問題タブ [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に印刷してもらいたい(A :\: A) :|: (A :&: B) = B
です。上記の出力は、次のコードによって得られます。
setDDr
驚いたことに、finset.vの元のコーディングを見ると、次のように括弧が付いています。
だから私はなぜ括弧が消えるのか、どのように Coq に CoqIde で括弧を明示的に出力させるのか疑問に思っています。
keyboard - Coqide キーバインドのバグ(?)
少し奇妙な問題が発生しています...最近、CoqIDE を使用しているときにいくつかの奇妙な状況が発生しています。
windows/superキーを押さないと文字「v」を入力できません。
複数のウィンドウが開いている場合、バックスペースを押すとフォーカスが前のタブに移動します。それで物事を削除することはできません。ただし、チャンクの削除には CTRL+backspace が機能します。
キーマップを US から GB に変更した後に最初の 2 つ (発生した可能性があります) が発生しましたが、前後に切り替えても問題は解決しませんでした。
ARCH Linux を実行すると、すべてが最新の状態になり、他のアプリケーションは影響を受けません。スティッキー キーはオンになっていません。
ご提案ありがとうございます。
編集:再インストールを試みましたが、役に立ちませんでした...
解決済みの編集: ええ、あなたは完全に正しいです。気付かないうちに超高速の再バインドを行ったようです。また、.config ファイルはアプリによって生成され、マネージャーの管轄下にないため、パッケージ マネージャーは基本的に .config ファイルに触れないことも学びました。解決しました!