Totality is optional in Idris. Also, the big dependently-typed languages like Coq, Agda, Idris all support corecursion, so they can run programs infinitely prov

Totality is optional in Idris. Also, the big dependently-typed languages like Coq, Agda, Idris all support corecursion, so they can run programs infinitely provided the program does something productive.