我想为(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)
这种方法合理吗?
**
当您要在第一个坐标上添加显式类型注释时,使用的语法糖有点笨拙。我只是DPair
直接使用:
NEqPa : Type -> Type
NEqPa a = DPair (a, a) $ \(x, y) => Not (x = y)
本文收集自互联网,转载请注明来源。
如有侵权,请联系 [email protected] 删除。
我来说两句