问题标签 [coqide]

Windows 10 中 wsl2 下的 Ubuntu 21.10 成功共享全局剪贴板内容（例如，在 nano 或 emacs 中），但 coqide（8.12.0，通过 apt 安装）没有。

我在配置中找不到任何关于剪贴板的内容，在我的本地 coqiderc 文件中也找不到。

在 github coq 存储库中有一个叫做CoqIDEWishes的东西，但我在那里也找不到任何关于它的东西。

这是一个常见问题还是特定于我的设置？我可以修理它吗？

一切都很好，直到我在 CoqIde 中更改了首选项 -> Externals -> coqtop，然后我发现自己在启动 CoqIde 时遇到了麻烦，如图所示。看来我在coqtop中写错了路径。我试图重新安装coqplatform，它似乎没用。那么如何重新启动我的 CoqIde？

我想在我的 CoqIde 中使用 HoTT 库。我的环境是Coq_Platform_2021.09.0.8.13-installer-windows-x86_64-signed，我尝试了很多方法。

1. 我尝试Require Import HoTT.在 CoqIde 中编写并得到错误Unable to locate library HoTT. (While searching for a .vos file.)
2. 我试着写From HoTT Require Import Basics.或者Require Import HoTT.Basics.我得到了错误Notation "~ _" is already defined at level 75 with arguments constr at level 75
3. 但是，我可以加载一些库，例如UnivalenceAxiom通过编写From HoTT Require Import UnivalenceAxiom. 所以我的问题是如何在我的 CoqIde 中导入 HoTT 库？

我想在 Coq 证明脚本中编写中间引理，例如，在 SCRIPTProof. SCRIPT Qed.本身内部 - 类似于在 Isar 中所做的。如何在 Coq 中做到这一点？例如：

我知道该exact声明并想知道是否是这样...但是我也希望像在 Isar 中一样拥有该声明的证据，have by auto或者using Proof. LEMMA_PROOF Qed.

为了使其具体化，我试图做这些非常简单的证明：

但我不确定它是如何工作的，而且效果不太好。

有关的：

• 我知道 Czar ( https://coq.discourse.group/t/what-is-the-difference-between-ssreflect-and-czar/824 ) 但 Coq afaik 不再支持。

我在我的消息栏中期待一些东西，但我没有看到它

示例脚本：

在 Jscoq 我看到（https://coq.vercel.app/scratchpad.html）：

在 vscode 我什么也没看到。

看图片清楚

叉：

• https://github.com/coq-community/vscoq/issues/280
• https://coq.discourse.group/t/how-to-activate-the-messages-window-in-vscode-like-the-coqide-has/1584