The article being discussed paints a very incomplete picture of what Idris does, but Idris seems to be in agreement with pron's comment here: it allows function

The article being discussed paints a very incomplete picture of what Idris does, but Idris seems to be in agreement with pron's comment here: it allows functions that loop forever, but if you want to write a proof, you'll need to ensure that it terminates. In fact, all functions are, by default, allowed to be partial. https://edwinb.wordpress.com/2013/02/19/on-partial-functions-in-idris/ https://edwinb.wordpress.com/2013/02/19/on-partial-functions...