agda-categories icon indicating copy to clipboard operation
agda-categories copied to clipboard
verified publisher icon pcapriotti

loading zero.agda

Open nrolland opened this issue 9 years ago • 3 comments

Hi,

I was trying to load your library with Agda version 2.5.1, standard library v0.12 and agda-base at 823c684 (2016-06-19) but it could not compile with error

/agda-categories/category/category/zero.agda:13,8-18

No instance of type Coercion (Bundle (IsGraph i j)) (Bundle (IsGraph (_i_6 i j W) (_j_7 i j W))) was found in scope.

It might be a stupid thing on my part, as I did not use agda for some time..

nrolland avatar Nov 03 '16 16:11 nrolland

I haven't updated this library in a long time. With the recent changes to instance arguments in Agda, the overloading mechanism that I was using should probably be redesigned and rewritten. It is probably going to require quite a lot of work before it can be typechecked again.

pcapriotti avatar Dec 15 '16 15:12 pcapriotti

Is there any way to point to a freezed Agda/Standard lib version which would make it work ?

nrolland avatar Dec 15 '16 15:12 nrolland

Probably Agda 2.3.2. The standard lib is irrelevant, because agda-categories does not use it.

pcapriotti avatar Dec 26 '16 14:12 pcapriotti