我在 VS Code 上使用Lean，这是一种开源定理证明器和编程语言。许多命令需要'\'编写数学符号，就像 LaTeX 一样。
Lean on VS Code 和 LaTeX 的本质区别在于，为了编译数学符号（例如，get\forall和数学'forall'符号之间的区别），当您在符号后面键入字符时，必须出现下划线\。
我遇到的问题是这个下划线
1) 在我输入时并不总是出现\
2) 消失得太快。
我的问题是：这是一个错误，还是有办法更改 VS 代码中的设置，使下划线始终出现在\?
任何答案将不胜感激。