Сопоставление образцов на продуктах в Идрисе

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

Но есть ли более прямой путь?

Answer 1

В https://github.com/idris-lang/Idris-dev/blob/master/docs/faq/faq.rst#i - очевидно, что программа завершается, но-идрис говорит-возможно-нет-всего-почему-то В ЧАВО явно упоминается, что идрис делает не считать (m, n) синтаксически меньшим, чем (S m, S n), и предлагает использовать assert_total в качестве выхода.

Существует также тип, который можно использовать для доказательства того, что какой-то другой тип сходится к базовому случаю, но я не могу вспомнить его название в настоящее время.