Zulip Chat Archive

Stream: general

Topic: lean.nvim does not highlight tactics


Matei Adriel (Apr 04 2022 at 10:49):

Hi! I am learning lean using the lean.nvim plugin. Is there any way to get it to highlight tactic code like the book?

Yaël Dillies (Apr 04 2022 at 11:12):

I'm sure @Julian Berman can pull it off.

Julian Berman (Apr 04 2022 at 13:43):

Hi hi. @Matei Adriel is this Lean 4 highlighting you're asking about? Or Lean 3?

Matei Adriel (Apr 04 2022 at 16:06):

@Julian Berman lean 4

Julian Berman (Apr 04 2022 at 16:44):

I see. For Lean 4 we're waiting for neovim to merge support for LSP syntax highlighting, which means it will be Lean itself that can draw proper syntax highlighting. That PR is here: https://github.com/neovim/neovim/pull/15723 so you can follow that.

Julian Berman (Apr 04 2022 at 16:44):

There are some things we could do in the interim but it's somewhat lower priority given that as soon as that PR (and a follow-up or two) is merged, things should just work.


Last updated: Dec 20 2023 at 11:08 UTC