4 ms·

What is “TC”?

• nextaccountic 3y ago
  Turing complete However it appears that Idris is Turing complete https://cs.stackexchange.com/questions/19577/what-can-idris-not-do-by-giving-up-turing-completeness https://cs.stackexchange.com/questions/19577/what-can-idris-... https://gist.github.com/porglezomp/b7bbbecbac1c2289fc890a53dfcec086 https://gist.github.com/porglezomp/b7bbbecbac1c2289fc890a53d... so I'm confused.
  • Quekid5 3y ago
    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.)