我想描述整数：
data Integer : Set where
Z : Integer
Succ : Integer -> Integer
Pred : Integer -> Integer
?? what else
上面没有定义整数。我们需要Succ（Pred x）= x和Pred（Succ x）= x。然而，
spReduce : (m : Integer) -> Succ (Pred m) = m
psReduce : (m : Integer) -> Pred (Succ m) = m
无法添加到数据类型。无疑，对整数的更好定义是，
data Integers : Set where
Pos : Nat -> Integers
Neg : Nat -> Integers
但是我很好奇是否有一种向数据类型添加方程式的方法。
似乎您想做的是Integers通过Succ (Pred m)用m等号标识的等价关系将您的类型定义为商类型。Agda不再支持它-有一个实验性的库试图做到这一点（通过强制商类型上的所有函数都需要通过需要表示不变性证明的辅助函数来定义），但是随后有人发现实现不够防水，因此可能导致不一致（基本上是通过访问假定的一种假设） （从外部无法访问），有关详细信息，您可以看到以下消息：
我们不确定这种破解是否正确。现在，感谢丹·多尔（Dan Doel），我知道不是。
[...]
鉴于这些观察，很容易证明上述假设是不正确的：
我认为，目前您最好的选择（如果您希望/需要坚持使用松散的表示形式，并使其等同于收紧），则是Setoid为您的类型定义一个。
本文收集自互联网，转载请注明来源。
如有侵权，请联系 [email protected] 删除。
我来说两句