Library Unusable to stdlib 1.1 Users ---`levelOfTerm` about agda-categories HOT 10 CLOSED

that being said, I think it is important to get the library clean in the first place. levelOfTerm is handy to keep universe level high-level. cleanup afterwards tends to be less optimal.

from agda-categories.

Note that the issue title is misleading: the problem is not the compiler version
but the standard library one.

from agda-categories.

See closed issue #10 for a discussion relating to this very topic.

from agda-categories.

oops. sorry

from agda-categories.

fixed in https://github.com/agda/agda-categories/tree/release/v0.1

from agda-categories.

I'm getting the following error using Agda 2.6.0.1, standard library 1.1 and the current master:

$ agda Everything.agda
/some-path/Categories/Category/Monoidal/Braided.agda:25,23-34
Not in scope:
  levelOfTerm
  at /some-path/Categories/Category/Monoidal/Braided.agda:25,23-34

from agda-categories.

I'm getting the following error using Agda 2.6.0.1, standard library 1.1 and the current master:

$ agda Everything.agda
/some-path/Categories/Category/Monoidal/Braided.agda:25,23-34
Not in scope:
  levelOfTerm
  at /some-path/Categories/Category/Monoidal/Braided.agda:25,23-34

stdlib has released 1.2. I think the master branch of this library works with that version.

from agda-categories.

I wonder if there is a way to put some code in Everything.agda to detect stdlib-1.2 (or lack thereof) early, so that we can fail gracefully?

from agda-categories.

one possible (and dumb) way is to maintain a Version-1.2.agda file in stdlib for example, so that this file should be loaded before anything.

from agda-categories.

Oops! I had not updated my .agda/libraries-2.6.0.1/ file. Thanks!

from agda-categories.