toothbrush/agda-gp — comment on commit 275c89c1fb23f97e285fb64e9cebdda9980afef7
File:  line 0
By marcelosousa:

What's wrong is this part:

-- xx = [[]]
-- xx should be:
-- xx = < inj₂ ( < inj₁ tt > , < inj₁ tt > )
xx : MyListList
xx = < inj₂ ( [] , < inj₁ tt > ) >

I believe this is caused by μType.

On Oct 31, 2011, at 6:08 PM, jpcooper wrote:

> What is wrong with μType?
>
> --
> Reply to this email directly or view it on GitHub:
> https://github.com/toothbrush/agda-gp/commit/275c89c1fb23f97e285fb64e9cebdda9980afef7#commitcomment-685354