|
|
|
|
|
|
by chriswarbo
1217 days ago
|
|
|
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.) |
|
|