any way to make vscode pulgin list the unicode symbol in ...

Stream: general

[onriv]

Hi is there any way to make vscode pulgin list the unicode symbol in complete list? #general

[Kevin Buzzard]

There's just a file somewhere on GitHub with the list

[onriv]

like this in emacs’s similar plugin https://github.com/vspinu/company-math

[Kevin Buzzard]

https://github.com/leanprover/vscode-lean/blob/master/src/abbreviation/abbreviations.json

[onriv]

Thank you very much.

[onriv]

Can we make it shown in vscode’s auto-complete candidate list?

[onriv]

got it with a similar plugin named latex input. Lean works with this plugin too. Cheers!