huwcampbell / idris-lens Goto Github PK

I'm trying to use this package in my project and I'm not sure how to properly install/import it.
The official documentation doesn't mention anything about installation of third party libraries.

Juts putting "-p lens" in my opts field of my project ipkg also doesn't seem to be working.
After typing idris --build myprojectname.ipkg I'm getting:

The following packages were specified but cannot be found:
- lens

Any reason to have two separate repos? https://github.com/idris-hackers/idris-lens

This is in base and would work perfectly well. This also means requiring no dependencies at all to write a lens in another library.

I appreciate you haven't looked at this library for a long time however if you are still interested, I've been trying to get it to work with Idris 2. I have only one function left that's giving me issues (apart from Examples.idr but I think that will be easier to solve). The last error can be seen by getting the master branch from https://github.com/shmish111/idris-lens and trying to build with idris2 idris2 --build lens.ipkg