style: proof style improvements in RegexSpec.lean
Nobody has claimed this yet.
Assessment
- Difficulty
- 4/5
- Estimated time
- 3-5 days
- Newbie friendliness
- 35/100
- Issue type
- Refactor
- Clarity
- Mostly clear
- Activity status
- Stale
- Domain
- compilers
Research direction
Read RegexSpec.lean, starting with regex_match_sound and the Glushkov proofs, then compare the specialized lemmas with the general lemmas in Matcher.lean. Review the DecidableEq branches and the discarded dr binding; done means the comments, robust proof cases, and general-lemma reuse are applied without changing proof behavior.
Written by the indexing model from the issue text.
Description
Items
Low-priority style items flagged by AI code review on PR #9.
1. Unused dr binding in regex_match_sound
regex_match_sound destructs the regex_match_correct result with obtain ⟨ast, _, h_parse, _, h_match⟩ — the _ discarding dr is fine. However, a comment noting why dr is intentionally discarded (we only need the AST-level match) would help readers understand the relationship.
2. Fragile DecidableEq instance comparison
Some proof branches use pattern matching on DecidableEq results that could be made more robust with cases, simp, and Subsingleton.elim to avoid depending on instance resolution order.
3. Specialized lemmas that could use general ones
Some lemmas in the Glushkov submodule have specialized proofs for things that general mathlib lemmas already cover. Replace with calls to general lemmas from Matcher.lean.
References
- Flagged by AI code review on PR #9
- Dominant language
- Lean
- Stars
- 2
- Forks
- 1
- PR merge metrics
- No merged PRs in 30d
Contributor guide
No contributing guide indexed for this repository
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
More from lambdaclass/lambda_compiler_kit
-
Difficulty 1/5 Under an hour Newbie friendliness 72/100
-
Difficulty 1/5 Under an hour Newbie friendliness 68/100
-
Difficulty 2/5 1-3 hours Newbie friendliness 68/100
-
enhancement
Difficulty 4/5 3-5 days Newbie friendliness 48/100
-
Difficulty 2/5 1-3 hours Newbie friendliness 50/100
All issues in lambdaclass/lambda_compiler_kit
Similar issues
-
Difficulty 2/5 1-3 hours Newbie friendliness 75/100
-
internal.h中，漏掉了1个定义。 Open
Difficulty 1/5 Under an hour Newbie friendliness 95/100
-
Difficulty 2/5 1-3 hours Newbie friendliness 88/100
-
Difficulty 2/5 1-3 hours Newbie friendliness 88/100
-
Difficulty 2/5 1-3 hours Newbie friendliness 88/100
oxc-project/oxc#26944 ·