[SkySkimmer]

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.h...

[chriswarbo]

Oops, 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.)