>Idris won't reduce partial functions at the type level, in order to keep type checking decidable. Totality precludes Turing-completeness. Specifically, functi

>Idris won't reduce partial functions at the type level, in order to keep type checking decidable. Totality precludes Turing-completeness. Specifically, functions that don't terminate are by definition partial, and if you can't express functions that don't terminate then it isn't Turing-complete.