Skip to content
This repository has been archived by the owner on Nov 19, 2023. It is now read-only.

loading zero.agda #1

Open
nrolland opened this issue Nov 3, 2016 · 3 comments
Open

loading zero.agda #1

nrolland opened this issue Nov 3, 2016 · 3 comments

Comments

@nrolland
Copy link

nrolland commented Nov 3, 2016

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..

@pcapriotti
Copy link
Owner

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.

@nrolland
Copy link
Author

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

@pcapriotti
Copy link
Owner

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

Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants