(x,y)的类型是什么（其中x和y不相等）？

Question

我想要创建一种对于 (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)

这种方法合理吗？

- fweth

Answer 1

**的语法糖在第一坐标上添加显式类型注释时使用起来有些棘手。我会直接使用DPair：

NEqPa : Type -> Type
NEqPa a = DPair (a, a) $ \(x, y) => Not (x = y)

- Cactus

---

谢谢。如果我想详细了解Idris的语法，您能推荐一些资源吗？目前还没有语言报告，是吗？ - fweth