Re: [Agda] Why does Data.Product have � for the type constructor?

Lennart Augustsson lennart at augustsson.net
Fri May 9 19:27:18 CEST 2008


It might look baffling, but it's the right thing.

2008/5/9 Samuel Bronson <naesten at gmail.com>:

> Why does Data.Product have $B-t(B for the type constructor? Wouldn't $B&0(B be
> more appropriate? I guess that might have other connotations,
> though... still, $B-t(B???
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20080509/b159d9d1/attachment-0001.html


More information about the Agda mailing list