[Agda] some yellow, for your amusement

[Ulf Norell]

On Fri, Jul 25, 2008 at 12:24 PM, Conor McBride <conor at strictlypositive.org>
wrote:

> Dear friends
>
> I append some comical scribblings that I dreamt up down the
> pub and typed in this morning. Nothing to get excited about:
> the kit all typechecks but the example at the end doesn't.
>
> I think it's a bunch of unsolved constraints that are holding
> things up. More particularly, I suspect that
>
>  f (x , y) = t
>
> is not being solved (for f) in situations where
>
>  f x y = t
>

Yep, that won't get solved.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20080725/b3407c76/attachment.html