小编Kri*_*ian的帖子

我使用Vim来编写我的.tex文件,但是在使用Vim中的拼写检查程序时遇到了问题.有时它不检查单词,我认为可能是由于以下原因.

由于Vim显然不应该检查.tex文档中的所有单词,例如,不是前导码,它只检查某些区域中的拼写(在语法意义上).正如我从这里收集的那样,其中一个地区是texSectionZone.这些区域可能变得非常大,实际上通常是一个区域,所以Vim很难意识到它实际上是在某个texSectionZone区域(或其他区域),因此不会检查拼写.如果我在文档中进行搜索,或者跳过多行(或更确切地说是页面)的任何类型的跳转,都会发生这种情况.

我得出结论的方式可能是以下原因:我知道命令

:echo synIDattr(synID(line("."),col("."),1),"name")

打印你所在的地区/地区的名称(我在这里找到了),所以当拼写检查工作不起作用时我尝试了这个,它告诉我它根本不在任何地区.它工作的地方,我在一个应该检查拼写的区域.

到目前为止,我唯一的解决方案是找到我希望拼写器检查的点上方最近的部分,然后手动将光标向下移动到给定点.

理想情况下,我非常想要一个确保不会发生这种情况的解决方案,但我也会选择一种方法来手动使vim'更新'它所在的区域,而不必移动光标.在后一种情况下,我正在考虑一种可以用于捷径的解决方案.

PS我怀疑该怎么称呼这个问题.如果你想出一个更好地解释问题的标题,可以随意改变它.

如果你没有给出:colorscheme一个参数,那么它会显示vim当前使用的colorscheme的名称.在vim中是否有类似的方式来显示是否设置了选项,或者如果它不是布尔值,则选项的值设置为什么？例如,如果我想知道是否autoindent已经设置或者我想知道它的价值textwidth,我该如何找到它？

说我有一个包含单词red和的文字blue.

如何更换这个词的出现次数blue字green只有在包含所有字线red？

同样我怎么能代替blue用green在不包含字都行red？

我试图在R中绘制一系列点,我type="b"用作绘图选项.然而,在点和它们之间的线之间存在大量填充(空白空间),以至于线在某些点之间完全消失.她的照片看起来像是:

我试图通过cex绘图选项使点更小,但这没有帮助,因为它只改变点的大小而不是这些点之间的点之间的线开始和结束的位置.我不知道这是否有所作为,但我使用的符号是pch=1.

我有兴趣知道是否可以减少这种填充,以及你如何做到这一点.我对使用type=o情节选项不感兴趣.

我发现我自己（有点）重复代码，因为我希望在目标和假设匹配时采用相同的策略。例如：

match goal with
| H : PATTERN |- _ => simpl in H; rewrite X in H; ... ; other_tactic in H
| |- PATTERN       => simpl     ; rewrite       ; ... ; other_tactic
end.

如果匹配案例中的策略变得很长，我基本上会重复它，并in添加一些子句，这看起来很不令人满意，特别是如果我有很多匹配子句，这样我就会重复很多代码。

有时并不是因为我匹配，而只是因为我定义了自定义策略，但根据上下文，我想将其应用于目标或命名假设。例如：

Ltac my_tac      H := simpl in H; rewrite X in H; ... ; other_tactic in H.
Ltac my_tac_goal   := simpl     ; rewrite X     ; ... ; other_tactic.

然后我再次“复制”代码。

有什么方法可以避免这种重复吗？

在某些时候，我想知道目标是否有一个名称，例如GOAL假设，因此simpl in GOAL相当于simpl，但我怀疑情况并非如此。在这种情况下，我可以删除 的定义my_tac_goal，然后直接调用 …

在vim中有没有办法读取文件,比如:r,然后将它存储在某个寄存器中？有没有办法做同样的事情,但只有文件中的行匹配某些模式？

当查看具有可判定相等的类型的结果时（特别是在Eqdep_dec中），有一些结果（对于类型A）需要

  forall x y : A, x = y \/ x <> y

而有些则需要

  forall x y : A, {x = y} + {x <> y}

我的印象是它是最后一个被称为可判定的相等，但我非常不确定有什么区别。我知道x = y \/ x <> y在Prop和{x = y} + {x <> y}中Set，并且我可以从第二个证明第一个，但反之则不行。据我了解，这是因为我不允许Prop从 type 的值构造 type 的值Set。

谁能说出两者之间有什么区别？是否有一些类型的示例可以证明第一个陈述但不能证明第二个陈述。另外，版本真的{x = y} + {x <> y}是所谓的可判定相等吗？

我是 Coq 的新手，试图弄清楚如何使用它Program来更轻松地定义事物，然后解决义务，但是，有时我会因为某些信息丢失而留下无法解决的义务。

例如，如果我定义以下内容（有点做作，但是我能想到的最简单的例子），那么函数 f 是一个接受两个相同偶数并返回该数字的双倍的函数。

Program Definition f {n : nat} (k1 k2 : {j : nat | j + j = n}) : {j : nat | j = n} := k1 + k2.
Next Obligation.

问题是，当我开始解决第一个义务时，这就是我剩下的

  k1, k2 : nat
  ============================
  k1 + k2 = k2 + k2

显然无法解决，因为我已经丢失了 的信息k1 + k1 = k2 + k2，并且我只能证明两个任意自然数相等。

为什么会发生这种情况？在这种情况下你会做什么来让 Coq 记住“所有假设”？