G. Allais

It won't work on windows but I'm keeping it as simple as possible in the hope it'd work on any unix style system. So far we only need simple things...

I am quite happy with the current script. I have included a command you can copy/paste in a terminal to test it.

Hmm. I think `defaults-2.9.0` is not actually supported by Agda. Meaning the only solution is to shove `standard-library` in the global `defaults` even though it may not be installed for...

> I suspect Agda may have a better approach by asking the user to expand the LHS and point out the empty bit with (). 💯 > But doing that...

Try using `absurd prf` on the RHS instead of `impossible` on the LHS. This will keep the pattern-matches in the case tree and help the coverage checker see that everything...

I'm happy with the current feature. I just need to take the time to hide this functionality behind a keystroke because it's (understandably?) a bit slow.

I've switched to a new branch after rebasing against current stable to take advantage of the caching of warnings in interfaces. I think I'm going to use the [`WarningMode`](https://github.com/agda/agda/blob/master/src/full/Agda/Interaction/Options.hs#L92) for...

So I got something working on https://github.com/agda/agda/tree/issue2503-useless-imports however: - [ ] the highlighting is not preserved through reloads - [ ] modules that are opened `public` are erroneously reported as...

I'm not sure I see the point of this type of PR: * it touches a lot of files which makes reviewing involved * it breaks downstream projects which makes...

Do you have a suggestion?