coq - 花括号 {} 在 ssreflect 中做了什么重写

Question

我正在阅读和玩 ssreflect 教程，遇到了使用 {} 引用的东西，我不太明白：

Variables P Q : bool -> Prop.
Hypothesis P2Q : forall a b, P (a || b) -> Q a.
Goal forall a, P (a || a) -> True.
  move=> a HPa. move: {HPa} (@P2Q _ _ HPa) => HQa.

谁能解释一下{HPa}做什么HPa？

顺便说一句，上下文是要引入“观点”？？？。我尝试删除{}，它仍然有效，但会产生不同的东西。而且我不知道在哪里可以找到诸如括号之类的文档@。

Answer 1

经过一些实验和比较，在 Coq 术语中似乎{H}是 to的功能。clear H.

move: {HPa} (@P2Q _ _ HPa) => HQa.

给

1 subgoals
a : bool
HQa : Q a
______________________________________(1/1)
True

尽管

move: (@P2Q _ _ HPa) => HQa.

给出相同的东西，除了HPa在上下文中保持不变：

1 subgoals
a : bool
HPa : P (a || a)
HQa : Q a
______________________________________(1/1)
True