Zulip Chat Archive
Stream: mathlib4
Topic: Goal markers in Lean/neovim
Antoine Chambert-Loir (Apr 16 2025 at 08:42):
I am getting used to the goal markers in Lean/Neovim.
Is there any way to have definitions marked with something as well?
Notification Bot (Apr 16 2025 at 08:42):
This topic was moved here from #mathlib4 > Goal markers by Antoine Chambert-Loir.
Last updated: May 02 2025 at 03:31 UTC