coq - 什么是 [...] 一般证明，为什么我不能删除它

Question

当我尝试复制粘贴验证代码时，有时会出现 [...]（即使我没有复制任何此类内容）并且我无法删除它。我必须撤消副本才能摆脱它。这是什么意思？

谢谢。

Answer 1

正如评论中所确认的，[…]这里的出现对应于 company-coq 的代码折叠功能。

切换块的可见性（从大括号开始，例如

Goal True /\ True.
split.
{ […]

或从子弹开始，例如

Goal True /\ True.
split.
- idtac. […]

)，您只需将点移动到开始符号{或-，然后按RET

否则，要“展开”环境缓冲区的所有块，您可以执行以下操作：

M-x company-coq-features/code-folding-reset-to-initial-state RET