Hacktoberfest 2026: the issues maintainers tagged for October, open and beginner-friendly. Browse Hacktoberfest issues

Non-tactic `stop` shouldn't be highlighted in red

Open Beginner friendly
  • Is something wrong?
#564 0 comments 0 reactions 0 assignees View on GitHub

Nobody has claimed this yet.

Assessment

Difficulty
2/5
Estimated time
1-3 hours
Newbie friendliness
70/100
Issue type
Bug
Clarity
Clearly specified
Activity status
Active
Tech stack
lua, neovim
Domain
developer-experience

Research direction

The payload does not name the file, so start by finding where the plugin's Lean highlight rules map the stop keyword to an error-style group (look in the tree-sitter highlight queries or the highlight setup). The example to check is the start stop usage at src/Init/Data/Array/Lemmas.lean lines 561-567 in the lean4 repository. Done when stop is highlighted as a normal keyword outside tactic blocks, while tactic stop keeps its current highlighting.

Written by the indexing model from the issue text.

Description

As in the title.

start stop is frequently used for array bounds, such as in

https://github.com/leanprover/lean4/blob/387908cb61eca4b499242240eda2dde1ebc589f9/src/Init/Data/Array/Lemmas.lean#L561-L567

Dominant language
Lua
Stars
607
Forks
63
Avg merge
3d 14h
Merged PRs (30d)
7

Getting set up

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

More from Julian/lean.nvim

All issues in Julian/lean.nvim

Similar issues

More Lua issues

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.