Ting-gian LUA

@jonas-frey, thanks for reporting this. Are you using Windows?

Does this happen in Agda files, or/and files other than Agda?

Thanks for the feedback! I added that debug buffer a while ago because my colleagues needed it for hacking Agda. Looks like you are doing something interesting, too 👀

Thank you for reporting this. I've been able to reproduce the problem. The condition for triggering the Unicode input mode when typing `\`, could depend on this [context](https://code.visualstudio.com/api/references/when-clause-contexts) thing. We...

You are right, if we type `\==q`, since there's no sequence that starts with `\==q`, it would stop and leaves `≡q` behind. But `\` somehow isn't treated the same as...

This is gonna get hairy!

This is definitely on the roadmap. It's a nightmare to ask dozens of students to install Agda on their machine. The good news is, it seems like users don't even...

I think we can have it enabled by default (like in Emacs), and have an option in the settings for disabling it.

Thanks for reporting this. Can you give us one example for autocompletion and one for case splitting?

Autocompletion failed because VS Code doesn't know what constitutes a valid token in Agda. You can also double click on names, and VS Code would select a group of characters...