4 ms·
Did HN eat the delay symbol? I don't think a regular "data" would work for this. https://agda.readthedocs.io/en/v2.6.3/language/coinduction.html#old-coinduction
by SkySkimmer 4y ago
Did HN eat the delay symbol? I don't think a regular "data" would work for this.
https://agda.readthedocs.io/en/v2.6.3/language/coinduction.html#old-coinduction https://agda.readthedocs.io/en/v2.6.3/language/coinduction.h...
- chriswarbo 4y agoOops, yeah; I know Agda needs special handling for codata (co-patterns, sharp/flat, etc.) Ironically, I'm more familiar with using codata in Coq; even though it's notoriously under-supported (breaking subject-reduction, no alternative to cofix, etc.)