Organize examples with native_decide lint disabled
Nobody has claimed this yet.
Assessment
- Difficulty
- 3/5
- Estimated time
- 1-2 days
- Newbie friendliness
- 55/100
- Issue type
- Refactor
- Clarity
- Mostly clear
- Activity status
- Stale
- Domain
- compilers
Research direction
Start with CharCorrectness.lean and inspect how its proofs and examples are organized. Refactor the file so a dedicated Examples section appears at the end, with native_decide lint disabled there; keep theorems and core library code outside it. Check other proof files for the same pattern as examples accumulate.
Written by the indexing model from the issue text.
Description
Summary
Create a dedicated section Examples in each proofs file to contain example assertions that use native_decide without triggering the linter.style.nativeDecide lint that applies to the rest of the codebase.
Approach
Use section with lint option disabled:
- Theorems and core library code remain strict (no native_decide)
- Examples use native_decide for quick verification without linter noise
- Clear signal about code intent and verification guarantees
Files to refactor
- CharCorrectness.lean
- (other proof files as they accumulate examples)
Notes
- Place examples section at end of file
- Examples should be non-library assertions only
- Theorems stay outside this section and use traditional proofs
- 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 ·