如果我试图证明Nat和Bool在Agda中不相等: open import Data.Natopen import Data.Emptynoteq () 我得到了错误: Failed to solve the following constraints:
Is empty: ℕ ≡ Bool 我知道不可能对类型本身进行模式匹配在Agda中有没有办法证明这一点?或者是不支持Agda中涉及类型的不等式?
但我仍然很困惑,我希望有一个没有Agda的解释,但直接脱离它的数学公式。(c : ∀ x → C x x refl) →,注意到最后一行要求我们提供x、y和p,那么为什么或者说,为什么第二个x是用x而不是y写的呢?
事实上,我已经考虑过这个问题,并得到了我的解释,但我不能确定我是否正确。J的类型签名是在命题世界,但它的定义是在判断世界。但如果我的推理完美无缺,回顾一下这个问题,我们为什么要写作?