小编Qin*_*ang的帖子

我想在两个不同的窗口中打开同一个文件夹。我在第一个窗口中打开了该文件夹，但是当我尝试在第二个窗口中打开该文件夹时，VS Code 只是跳转到第一个窗口，而不是在第二个窗口中打开它。

我想这样做是因为我想将文件分成两个窗口，并且我正在使用 VSCoq，这需要 VS Code 打开特定文件夹才能工作。

在Coq中,命题是类型,证明是值.例如,我们可以写一个像这样的简单证明,证明了这一点0=0.

Definition test : (eq 0 0) := eq_refl 0.

有趣的是,当检查其类型时eq_refl,它会显示出来

eq_refl
     : ?x = ?x
where
?A : [ |- Type] 
?x : [ |- ?A]

这意味着所有的论据eq_refl都是隐含的.在Coq中,除非使用隐式参数,否则通常不允许显式确定隐式参数@.为了证明0=0,我们可以明确地@eq_refl nat 0或只是eq_refl作为nat并且0可以推导出来.但在开始的例子中,eq_refl 0也有效.为什么？

这件事一般不起作用,例如

Definition foobar {A : Type -> Type} {T : Type} :  list (A T) := [].
Definition test : list (list nat) := foobar.
Fail Definition test' : …