2 ms·
Totality and non-standard recursion in Idris
- BalinKing 3y agoOnly tangentially related to the article, but Agda does allow termination checking to be disabled on individual functions: https://agda.readthedocs.io/en/latest/language/termination-checking.html https://agda.readthedocs.io/en/latest/language/termination-c...