Parse error with agda 2.5.2
MirceaS opened this issue · 4 comments
Hello!
I tried loading your library with agda 2.5.2 but I got this error:
.../categories/Categories/Power.agda:163,1: Parse error
overlap
: ∀ {D E} (H : Bifunctor D D ...
It's very weird as it looks completely innocuous.
Are you aware of this? Do you have any idea as to what might be causing it?
I can reproduce it. The problem is that, since 2.5.2, overlap is a new keyword in Agda. So this name will have to be changed. I tried to change it to overla (as a test!), and it all worked fine.
I'll probably rename it overlap', as it gives a PowerEndo' anyways. But I may not be able to do this right away.
Right. I changed that and it worked but then I ran into another issue in Comma.agda
.../categories/Categories/Comma.agda:28,19-36
Data.Product.Σ
((_h_440 T S A.∘ _g_439 T S) A.∘ _f_438 T S A.≡
_h_440 T S A.∘ _g_439 T S A.∘ _f_438 T S)
(_B_433 T S)
!=< (.h ∘′ .g) ∘′ .f ≡′ .h ∘′ .g ∘′ .f of type Set (e₂ ⊔ e₁)
when checking that the expression A.assoc , B.assoc has type
(.h ∘′ .g) ∘′ .f ≡′ .h ∘′ .g ∘′ .f
I commented most of the file out and then managed to Load Everything so I don't think there will be anymore issues besides this. If you could look into it, that'd be great.
Possibly a completely separate issue - but I'll look at that too.
This was fixed by PR #17