Comments (10)
Can you elaborate on what you mean? This plugin does have support for entering unicode abbreviations already. What functionality are you missing?
from lean.nvim.
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.
from lean.nvim.
It works exactly the same way. Feel free to come ask on the Lean Zulip if you're having setup issues.
from lean.nvim.
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?
from lean.nvim.
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.
from lean.nvim.
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.
from lean.nvim.
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.
from lean.nvim.
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.
from lean.nvim.
Are you using vim? This is a neovim plugin.
from lean.nvim.
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.
from lean.nvim.
Related Issues (20)
- Find executable via `elan which` HOT 7
- Anonymous sections aren't treated as a pair HOT 1
- "Try this" replaces incorrect segment HOT 6
- Consider making the max width / height of infoviews work via percentages of real estate rather than columns/rows
- Improve `:Telescope loogle` HOT 1
- highlights.scm: @boolean -> @constant.builtin.boolean, @repeat -> @keyword.control.repeat HOT 4
- Help for a newbie HOT 3
- Client 1 quit with exit code 0 and signal 11 HOT 5
- Infoview autoclose HOT 1
- Musl usage error message HOT 4
- Inaccessible hypothesis highlighting should highlight inaccessible names even when there are alternate accessible ones
- (Re-)review / harmonize with the VSCode options
- Infoview tooltips should render their contents as markdown HOT 1
- Spawning language server with cmd: `lean` failed HOT 1
- Set winfixbuf when available (0.10+) on our infoview windows.
- Files opened under */src/lean/ are unmodifiable HOT 9
- Entering edit mode will shrink line-number bar, moving text around HOT 3
- How can i help the project? HOT 5
- Deprecated Commands in Neovim 0.11 HOT 1
Recommend Projects
-
React
A declarative, efficient, and flexible JavaScript library for building user interfaces.
-
Vue.js
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
-
Typescript
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
-
TensorFlow
An Open Source Machine Learning Framework for Everyone
-
Django
The Web framework for perfectionists with deadlines.
-
Laravel
A PHP framework for web artisans
-
D3
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
-
Recommend Topics
-
javascript
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
-
web
Some thing interesting about web. New door for the world.
-
server
A server is a program made to process requests and deliver data to clients.
-
Machine learning
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
-
Visualization
Some thing interesting about visualization, use data art
-
Game
Some thing interesting about game, make everyone happy.
Recommend Org
-
Facebook
We are working to build community through open source technology. NB: members must have two-factor auth.
-
Microsoft
Open source projects and samples from Microsoft.
-
Google
Google ❤️ Open Source for everyone.
-
Alibaba
Alibaba Open Source for everyone
-
D3
Data-Driven Documents codes.
-
Tencent
China tencent open source team.
from lean.nvim.