If my understanding is correct, Agda and Coq disallow general recursion, so all programs terminate by construction, but Idris relaxes this, in a desire to be more pragmatic at the cost of not as clean mathematically (functions have to be modeled as partial in general, to account for the fact they might not terminate).

General recursion, yes however often the fixed point operator is added (and its associated judgements) to have interesting programs/proofs.

Hmm, that fixed point operator, rings a bell, can't quite put my finger on it . . . :-)