undefined | Better HN

0 pointskazagistar10y ago0 comments

From what I know, Idris does not have this constraint: you are free to introduce nontermination wherever.

0 comments

You're correct that Idris doesn't force termination. That doesn't let you compute non-computable functions though (e.g. the busy beaver function).

j / k navigate · click thread line to collapse

0 pointskazagistar10y ago0 comments

From what I know, Idris does not have this constraint: you are free to introduce nontermination wherever.

You're correct that Idris doesn't force termination. That doesn't let you compute non-computable functions though (e.g. the busy beaver function).

j / k navigate · click thread line to collapse