3 ms·
Almost arbitrarily - they must be computable... ;)
by dllthomas 11y ago
Almost arbitrarily - they must be computable... ;)
- kazagistar 11y agoFrom 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).