Agda's type system is not turing complete, you can only run on the type-level functions that are proven to be terminating [1] (using well-founded induction or c

Agda's type system is not turing complete, you can only run on the type-level functions that are proven to be terminating [1] (using well-founded induction or co-induction). Same for Coq, and probably Idris. [1]: http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.Totality http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceMa...