Coq 中的“eq^~”是什么意思？

Question

当我写作时 '打印 Qeq_trans。'在 CoqIde 中，我可以在消息窗口中看到许多 'eq^~' 表达式。

例如，eq^~ (Qnum z * QDen x * QDen y)%Z。

请告诉我这个词的意思。

Answer 1

我认为这是一种仅将函数应用于其第二个参数的方法。做一个

Locate "_ ^~ _".

获取定义。