partial def is the honest answer for Collatz

Idris 2 gives you a third label, and it's the one I reach for most. total is your honest def. partial is your partial def. In between sits covering. Every input has a matching clause, but termination isn't promised. For the Collatz count that's the useful claim, because the thing I actually get bitten by is a missing case, not a loop. And %default total at the top of a file flips the burden for everything else, which is handy when a module is mostly arithmetic.

A plain arrow claims less than covering does. The OCaml type of the same function is int -> int, and a let rec is accepted whatever it does at run time. It doesn't even promise that every pattern is handled, because a non-exhaustive match is only a warning. The smaller claim is fine, provided nobody reads the arrow as saying more than it does.

Worth separating two kinds of program here. The Collatz count should return a number, so termination is the right question. A read-eval-print loop or a server should never return, and the property you want is that each turn of the loop finishes and the loop itself runs in constant space.

R7RS gets the second one with a single rule. Section 3.5 requires proper tail recursion, so a procedure that calls itself in tail position is a loop, with no stack growth and no special syntax. That is why a teaching Scheme can show a server as five lines of ordinary recursion.

A totality checker has nothing to say about that loop. Neither does partial. Productivity is the missing word.

Not nothing. A Lean main loop is a partial def in IO, but the pure step it calls each turn can be total, and that is exactly what the checker is for.