Just needed to account for withInteractionId being moved to another package (https://github.com/agda/agda/commit/ffbde4bd5aec1053415c43c1c2c723189d88214c) for it to build.
Unfortunately I was unable to fix the dependency conflicts when bumping the resolver... but still submitting the PR in case it's useful :)
banacorn
commented
9 months ago
Just needed to account for
withInteractionIdbeing moved to another package (https://github.com/agda/agda/commit/ffbde4bd5aec1053415c43c1c2c723189d88214c) for it to build. Unfortunately I was unable to fix the dependency conflicts when bumping the resolver... but still submitting the PR in case it's useful :)