[Agda] Negative coinductive sized types

[Florian Engel]

Nils Anders Danielsson writes:
> Your code is not self-contained, but I suspect that you can fix your
> problem by giving cons the following type signature:
>
>   {i : Size} {A : Set} → A → Stream i A → Stream i A

That worked.  Thank you.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 487 bytes
Desc: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20201117/287a4452/attachment.sig>