可在此处找到的Coq标准库文件Coq.Init.Logic 包含该语句
Notation "A -> B" := (forall (_ : A), B) : type_scope.
鉴于符号->已经具有内置含义,我不明白这是如何可能的.被这->覆盖了吗？
如果我输入A -> B,Coq如何知道我的意思A -> B或forall (x : A), B？
是的,我知道这两个命题在逻辑上是等价的,但这不应该是一个定理而不是一个符号吗？
你可以说,我对Coq没有多少经验,但我想了解细节.
coq ×1