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