Jesper Cockx

@Zekt I tried to run this plugin from code-server as you described, I got code-server to run however I'm not able to install the plugin as you describe. It seems...

Ah I see, so there is already an issue for that. I managed to work around the problem by copying my local .vscode configuration to the code-server installation, but it's...

Welcome to submit a PR to add this to the documentation!

If @UlfNorell is also fine with this, I think it can be merged as-is.

That's indeed interesting. It seems plausible that this is indeed what's causing the performance issues. Three possible solutions I can see: - Don't use `instantiateFull` in performance-critical places - Cache...

@UlfNorell did you manage to find a solution for this?

Here is a minimized example: ```agda open import Agda.Builtin.Sigma data Ctx : Set₁ Env : Ctx → Set data Ctx where _∷_ : (Γ : Ctx) → (T : Env...

Here's an example of some work that could be avoided if we were able to use a state monad for a backend: https://github.com/agda/agda2hs/blob/f48bb1c9f4c0f22f02dd6d0c40b2d179ddf31678/src/Agda2Hs/Compile/Utils.hs#L123-L127

You're right, these would eventually have to be changed as well to be (more) useful with instance search. And having `overlap` on these fields would indeed be useful as well....

Some superclasses (such as the `Functor` superclass of `Applicative`) are not defined as fields at all, but are instead defined in terms of the functions of the subclass. So here...