Coq 中的“eq^~”是啥意思？
Posted
技术标签:
【中文标题】Coq 中的“eq^~”是啥意思？【英文标题】：What does "eq^~" mean in Coq?Coq 中的“eq^~”是什么意思？ 【发布时间】：2021-08-04 10:46:52 【问题描述】：当我写作时 '打印 Qeq_trans。'在 CoqIde 中，我可以在消息窗口中看到许多 'eq^~' 表达式。
例如，eq^~ (Qnum z * QDen x * QDen y)%Z。
请告诉我这个词的意思。
【问题讨论】：
【参考方案1】：我认为这是一种仅将函数应用于其第二个参数的方法。做一个
Locate "_ ^~ _".
获取定义。
【讨论】：
确实，f^~x 是 fun y => f y x以上是关于Coq 中的“eq^~”是啥意思？的主要内容，如果未能解决你的问题，请参考以下文章