伊德里斯：试图在总体检查失败重新实现fromInteger进行NAT

Question

我有以下代码：

module Test 
    data Nat' = S' Nat' | Z' 
    Num Nat' where 
    x * y = ?hole 
    x + y = ?hole 
    fromInteger x = if x < 1 then Z' else S' (fromInteger (x - 1)) 

我得到最后一行一条错误消息：

Test.idr:6:5: 
Prelude.Interfaces.Test.Nat' implementation of Prelude.Interfaces.Num, method fromInteger is 
possibly not total due to recursive path Prelude.Interfaces.Test.Nat' implementation of 
Prelude.Interfaces.Num, method fromInteger --> Prelude.Interfaces.Test.Nat' implementation of 
Prelude.Interfaces.Num, method fromInteger 

功能应总是给出结果，因为fromInteger的参数最终会变得足够小以选择第一种情况。但伊德里斯似乎并不了解这一点。这个函数有什么问题，我该如何解决这个错误？

Answer 1

n - 1不结构比n小，看到这只是观察Integer不是感应式。因此，你需要说服的全部检查你的函数使用了一招类似assert_smaller（见伊德里斯tutorial）实际上是总：

下面是它的current定义：

assert_smaller : (x : a) -> (y : b) -> b 
assert_smaller x y = y 

它只是计算其第二个论点，但也向整体检查者断言y在结构上小于x。

这是伊德里斯在其标准库使用（见here）为您的问题：

fromIntegerNat : Integer -> Nat 
fromIntegerNat 0 = Z 
fromIntegerNat n = 
    if (n > 0) then 
    S (fromIntegerNat (assert_smaller n (n - 1))) 
    else 
    Z