3 ms·
From what I know, Idris does not have this constraint: you are free to introduce nontermination wherever.
by kazagistar 11y ago
From what I know, Idris does not have this constraint: you are free to introduce nontermination wherever.
- kmicklas 11y agoYou're correct that Idris doesn't force termination. That doesn't let you compute non-computable functions though (e.g. the busy beaver function).