3 ms·
Brief nitpick: Idris and Agda both have codata constructions, and in Idris (at least, I'm not familiar with Agda) it is supported by the totality checker.
by icen 10y ago
Brief nitpick: Idris and Agda both have codata constructions, and in Idris (at least, I'm not familiar with Agda) it is supported by the totality checker.