[nextaccountic]

Turing complete

However it appears that Idris is Turing complete https://cs.stackexchange.com/questions/19577/what-can-idris-... https://gist.github.com/porglezomp/b7bbbecbac1c2289fc890a53d... so I'm confused.

[Quekid5]

Note the "codata" and also note that "main" is marked as "partial". Only the total subset of Idris is non-TC.

Note also the use of Fuel -- this is to provide "fuel" for the computation, but it's a data structure which can only decrease in 'size' -- which is used by the compiler to prove totality (termination).

("codata" is a way to model 'infinite' computations as data structures.)