codata #17

Open
opened 2023-06-15 13:15:28 -04:00 by rhi · 0 comments
Owner

big shrug

i would do a "agda copattern coinductive no-eta-equality record" type thing, but there is linearity in the mix. idk

big shrug i _would_ do a "agda copattern coinductive no-eta-equality record" type thing, but there is linearity in the mix. idk
rhi added the
language
label 2023-06-15 13:15:28 -04:00
Sign in to join this conversation.
No Milestone
No Assignees
1 Participants
Notifications
Due Date
The due date is invalid or out of range. Please use the format 'yyyy-mm-dd'.

No due date set.

Dependencies

No dependencies set.

Reference: rhi/quox#17
No description provided.