我想为x(= y)设置对(x,y)的类型.

我的想法是定义NEqPa：Type – >键入NEqPa a应该包含所有元素((x,y),p)x：a,y：a和p：(x = y) – >虚空.我尝试了以下两个版本：

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)

这种方法合理吗？

最佳答案 当你想在第一个坐标上添加显式类型注释时,**的语法糖有点难以使用.我直接使用DPair：

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