如何解决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
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。