[dllthomas]

Almost arbitrarily - they must be computable... ;)

[kazagistar]

From what I know, Idris does not have this constraint: you are free to introduce nontermination wherever.

[kmicklas]

You're correct that Idris doesn't force termination. That doesn't let you compute non-computable functions though (e.g. the busy beaver function).