Idris 声称以下代码并不完整:
data Foo = Bar (Maybe Foo)
foos : Foo -> List Foo
foos (Bar (Just foo)) = foo :: (foos foo)
foos (Bar Nothing) = Nil
我可以做
foos t@(Bar (Just foo)) = foo :: foos (assert_smaller t foo)
但这似乎是不必要的。显然,我创建的第一个 Foo
必须构造为 Bar Nothing
,后续构造只能以相同的方式或从现有项构造,因此这应该始终终止。
是否有一些类似的情况无法确定整体性,或者 Idris 还不能处理这种情况?
最佳答案
你是对的。 Idris 还不能处理这种情况。
关于idris - 这是 Idris 完整性检查器的限制,还是我遗漏了什么?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/43104446/