Unicode LaTeX tab completion

[chakravala]

The Julia vim plugin has tab completion from LaTeX to Unicode, why doesn't the Lean vim plugin have this as well? I recommend taking a look at theirs to see how you can do it let https://github.com/JuliaEditorSupport/julia-vim

[Julian]

Can you elaborate on what you mean? This plugin does have support for entering unicode abbreviations already. What functionality are you missing?

[chakravala]

The README has not made it clear to me how to activate these abbreviations. In the Julia vim plugin, I can simply type \times and then press the TAB key to have it replaced with unicode. This is the most natural way in my opinion, I don't know how to do it with this plugin based on the half sentence of information in the readme.

[Julian]

It works exactly the same way. Feel free to come ask on the Lean Zulip if you're having setup issues.

[chakravala]

Does this require some kind of LSP to be enabled? I prefer not to use any sluggish LSP, the Julia VIM plugin does not depend on any LSP for Unicode. Why not just explain how to use it here?

[Julian]

It does not, though Lean (the language) certainly assumes you are using it through an LSP.

Why not just explain how to use it here?

Please be less presumptuous? Have you tried using this plugin already or simply assuming? I have other things to do than walk you through it, though if you were a bit less rude it certainly wouldn't hurt.

[chakravala]

It does not, though Lean (the language) certainly assumes you are using it through an LSP.

It seems that it's possible to use lean by using lean --run in terminal, so an LSP in the editor is not required to be assumed.

Have you tried using this plugin already or simply assuming?

Yes, I have tried using this plugin and I don't understand how I can insert unicode from this instruction:

Abbreviation (unicode character) insertion (in insert mode & the command window accessible via q/)

So when I am in insert mode and have the phrase \times, how can that be transformed to Unicode?

Please be less presumptuous?

My only presumption is that I am not able to accomplish the unicode insertion

I have other things to do than walk you through it, though if you were a bit less rude it certainly wouldn't hurt.

I'm not sure what you think is rude here, I'm trying out lean.nvim and am not successful at the unicode insertion.

[Julian]

It seems that it's possible to use lean by using lean --run in terminal, so an LSP in the editor is not required to be assumed.

Every user of the language uses it through an editor with an LSP, the vast majority of whom (95% plus) doing so via VSCode. No one uses Lean through lean --run.

So when I am in insert mode and have the phrase \times, how can that be transformed to Unicode?

Hit tab or space, after having enabled the plugin.

[chakravala]

Then I don't quite understand how to enable this plugin. I am using vim pathogen, and have cloned the repository into ~/.vim/bundle/lean.nvim.

Syntax highlighting for lean seems to be enabled, so I am not sure what I'm missing to enable here.

[Julian]

Are you using vim? This is a neovim plugin.

[chakravala]

Yes, I am using vim, I was hoping this would be backwards compatible. The Julia Vim plugin is an example where they have unicode tab completion, so I was hoping it would inspire someone to do something similar for lean with vim.