1

此 Idris 函数无法成功检查整体性，但在我看来，似乎涵盖了所有情况。这是我在合并排序中的合并功能。

使用 Idris 1.3.3 版

错误。

*d:/home/projects/testidris/test> :total merge2
Main.merge2 is possibly not total due to:
    Main.case block in case block in merge2 at d:\home\projects\testidris\test.idr:11:22-47 at d:\home\projects\testidris\test.idr:12:22-31, which is not total as there are missing cases

伊德里斯。

module Main

record Mergeable where
    constructor MkMergeable
    left : List Nat
    right : List Nat

merge2 : Mergeable -> List Nat
merge2 (MkMergeable [] right) = right
merge2 (MkMergeable left []) = left
merge2 (input) = let MkMergeable (left) (right) = input;
                     (a1 :: a2) = left;
                     (b1 :: b2) = right in
                 if a1 < b1 then a1 :: merge2 (MkMergeable a2 right)
                 else b1 :: merge2 (MkMergeable left b2)
4

0 回答 0