Idris产品中的图案匹配

Question

定义

ZZ : Type
ZZ = (Nat, Nat)

然后下面的代码

ZZ_greater_than_zero : ZZ -> Bool
ZZ_greater_than_zero (Z, Z) = False
ZZ_greater_than_zero (Z, (S n)) = False
ZZ_greater_than_zero ((S m), Z) = True
ZZ_greater_than_zero ((S m), (S n)) = ZZ_greater_than_zero (m, n)

给我

10 | ZZ_greater_than_zero (Z, Z) = False
   | ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
ZZ_ord.ZZ_greater_than_zero is possibly not total due to recursive path ZZ_ord.ZZ_greater_than_zero --> ZZ_ord.ZZ_greater_than_zero

但是如果我定义相同的功能，则>

ZZ_greater_than_zero_alt : Nat -> Nat -> Bool
使用类似的模式匹配不会产生错误。通过定义

，可以解决此问题。

ZZ_greater_than_zero : ZZ -> Bool
ZZ_greater_than_zero (a, b) = ZZ_greater_than_zero_alt a b
但是还有更直接的方法吗？

定义ZZ：类型ZZ =（Nat，Nat）然后是以下代码ZZ_greater_than_zero：ZZ->布尔ZZ_greater_than_zero（Z，Z）=假ZZ_greater_than_zero（Z，（S n））=假ZZ_greater_than_zero（（S m）.. 。

Answer 1

在https://github.com/idris-lang/Idris-dev/blob/master/docs/faq/faq.rst#i-have-an-obviously-terminating-program-but-idris-says-it-possibly-isnt-total-why-is-that中，FAQ明确提到idris不认为（m，n）在语法上小于（S m，S n），并建议使用assert_total作为解决方法。