Andrey Klaus (Apr 27 2023 at 00:46): Andrey Klaus (Apr 27 2023 at 00:46):Hello!
In mathcomp book we have such a definition
Definition edivn_rec d :=
fix loop m q := if m - d is m'.+1 then loop m' q.+1 else (q, m).
It looks to me like m' is not a direct subterm of m (at least it is not obvious (isn't it??)).
Why then the guard does not complain here?
Andrey Klaus (Apr 27 2023 at 01:04):I was able to find this one https://proofassistants.stackexchange.com/questions/1428/formal-description-of-coq-s-termination-checker
if somebody can give a link to simpler description, would be great still.
Pierre Roux (Apr 27 2023 at 06:21):The positivity checker is able to find that Nat.sub m d is a subterm of m thanks to the way Nat.sub is written.
Last updated: Oct 13 2024 at 01:02 UTC