Idris，类型加法（增量）

Question

我怎样才能写出这样的函数

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

或类似的东西？

谢谢

Answer 1

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

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

其中 addOne 会 return 一些 Nat 的元组和一个证明，这个 Nat 确实是 S n。或者事后证明 属性：

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

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