Julian / lean.nvim

Neovim support for the Lean theorem prover
MIT License
278 stars 27 forks source link

Add a default mapping for `:LeanRestartFile` and related tips #357

Closed utensil closed 4 weeks ago

utensil commented 4 weeks ago

Zulip

Julian commented 4 weeks ago

Thanks! The style warning is markdownlint being silly, we only care about GitHub's parser. The wordings actually look fine to me too -- if you do care to add a test it should be pretty trivial to do so although we don't actually test all the mappings we set really currently, we just pick some single one and make sure it's properly mapped -- so I'm happy to merge this as-is and add a linter exception -- if you do have any other suggestions or improvements on this or anything though they're always welcome!

utensil commented 4 weeks ago

Thanks, I'll try to figure out how to set up the test tomorrow, and add the test.

utensil commented 4 weeks ago

Updated and tested locally from nvim, it seems to work!