search

Julian / lean.nvim

neovim support for the Lean theorem prover
MIT License
248 stars 25 forks source link

Inaccessible hypothesis highlighting should highlight inaccessible names even when there are alternate accessible ones #326

Closed Julian closed 1 month ago

Julian commented 8 months ago

I.e. with a hypothesis like:

ht right✝ : R✝ z t

right should get greyed but ht should not.