fO {k = 996} -- strange output about idris-dev HOT 4 CLOSED

Indeed - that's because there is a built in limit on how deeply the REPL will evaluate recursive functions, and you just happen to have hit it…

Edwin.

On 24 Nov 2012, at 17:08, Falko [email protected] wrote:

If I type, e.g. in the REPL, fO {k = 996}, the output contains some strange items:

... (S (boolElim (Builtins.!>#@Builtins.Ord$[Int] 1 0 (boolElim (intToBool (prim__eqInt 1 0)) EQ (boolElim (intToBool (prim__ltInt 1 0)) Builtins.LT Builtins.GT))) (S O) O) ...

Until 995 it is fine :)

Thank you, and kind regards. Zenon

—
Reply to this email directly or view it on GitHub.

from idris-dev.

So its a feature then?

from idris-dev.

Not really a feature, though the behaviour is intentional - it is left over from before the totality checker could decide for itself whether something was guaranteed to terminate. It should only behave like this on expressions that aren't known to terminate - so I will fix it now that the totality checker is more reliable.

from idris-dev.

As far as I can tell, this issue has been fixed. In latest master:

Idris> fO {k=996}
fO : Fin 997
Idris> fO {k=2000}
fO : Fin 2001

from idris-dev.