in stdlib-0.16 implicit argument of Lift is now explicit

Question

in stdlib-0.16 implicit argument of Lift is now explicit

Closed this issue 5 years ago · 4 comments

p-pavel commented 6 years ago

Categories/Lift.agda & Categories/Support/Equivalence.agda are affected

Answer 1 · 2018-12-30T14:12:32.000Z

I would certainly welcome PRs for these things!

Answer 2 · 2018-12-30T15:33:01.000Z

This is a breaking change -- it will break compatibility with the older versions of stdlib.

Probably it will be nice to have a new branch?

Anyway, I'm trying to fix all the issues I've reported (or at least investigate on them) and I'll issue PR after that. in the case of Lift it's simple but see above about compatibility concerns.

Answer 3 · 2018-12-30T15:39:20.000Z

I think most people upgrade their Agda versions. But certainly documenting the commit version of the version that works with stdlib-0.15 is worthwhile. I guess maybe even make an official release or something [not that I quite know how, yet]. A clear README is likely in order too.

Answer 4 · 2019-08-09T16:20:06.000Z

This library is now obsolete - and the newer version of the library has this problem fixed.