Idris，类型加法增量

问题描述

如何编写这样的函数

data Wrap : Nat -> Type where
  Wrp : n -> Wrap n

addOne : (n : Nat) -> Wrap (S n)
addOne {n} = Wrp (S n)

以这种形式

addOne : (n : Nat) -> S n
addOne {n} = S n

还是类似的东西？

谢谢

解决方法

addOne : (n : Nat) -> S n无效，因为返回类型不是类型，而是值。与您可能想要的最接近的东西

addOne : (n : Nat) -> (k : Nat ** k = S n)
addOne n = (S n ** Refl)

其中addOne将返回一些Nat的元组和证明，此Nat的确是S n。或随后证明该属性：

addOne : (n : Nat) -> Nat
addOne n = S n

addOneIsSucc : (n : Nat) -> addOne n = S n
addOneIsSucc n = Refl