Inputting the "agda input prefix" as a literal

[googleson78]

If I set my agda input prefix to e.g. v, how can I input a v? My current prefix is a backtick, and I cannot figure out how to input a backtick into my code 😅

[googleson78]

(backtick is also my localleader, if that's relevant)

[isovector]

I don't think there's any way, today! I'm open to suggestions for what you'd like to happen, though.

[googleson78]

The easiest way to get this, although a bit annoying, is to have a "timeout", i.e. if you press "agda input prefix" and wait for 1s, you just get the prefix input as a literal. This is what maps usually do in vim - if you do

inoremap asdf ...

and then input an a while in insert mode, you'll eventually get the a input as a character after waiting for a bit.