我想要创建一种对于
这种方法合理吗?
(x, y)
且 x ≠ y
的配对类型。我的构想是定义 NEqPa:Type → Type
,使得 NEqPa a
包含所有元素 ((x,y), p)
,其中 x : a
,y : a
,且 p : (x = y) → Void
。我尝试了以下两个版本:NEqPa a = ((x, y) : (a, a) ** (x = y) -> Void)
NEqPa a = ((x : a, y : a) ** (x = y) -> Void)
这两个语句看起来都在语法上有问题,但我不知道该如何修复它们。
[编辑] 我找到了一个解决方案:
NEqPa a = (p : (a, a) ** (fst p = snd p) -> Void)
这种方法合理吗?