backslash issue in VS Code

Stream: lean4

[Michał Zdunek]

This might be a stupid question, but when I try to type, for example, rw [\<- mul_assoc] to get a back arrow, VS Code shows me the message

unexpected token '\'; expected ']'Lean 4
Type \ using \\ or \setminus

Does anyone know what might be the issue?

[Henrik Böving]

I don't know all the unicode shortcuts in vscode but the one I usually use for unicode left arrow is \l what about that?

[Michał Zdunek]

Nevermind looks like it works if I type with \ from the start, instead of adding the backslash to an existing expression - sorry for bothering you!

[Johan Commelin]

Btw, note that \l also works for this particular symbol.