refactor: eliminate decreasing_by in Parser.lean in favour of structural recursion
还没有人认领这个 Issue。
评估
- 难度
- 4/5
- 预计耗时
- 3-5 天
- 新手友好度
- 42/100
- Issue 类型
- 重构
- 描述清晰度
- 基本清楚
- 活跃度
- 停滞
- 领域
- compilers
调研方向
打开 Lck/Regex/Parser.lean，检查第 646 行和第 912 行的解析代码，然后阅读 CLAUDE.md 中关于终止性的指导。确定受影响的递归调用是否可以使用结构上更小的 token 列表；完成的标准是移除 decreasing_by 的两处用法，或者由解释性注释记录为什么无法进行重构。
由索引模型根据 Issue 内容生成。
描述
Problem
Lck/Regex/Parser.lean at lines 646 and 912 uses decreasing_by to convince the termination checker. Per CLAUDE.md, decreasing_by is a code smell for parsers — a well-structured LL(1) parser over a token list should terminate structurally.
Expected fix
Restructure the affected parsing functions so that recursive calls are made on a syntactically smaller token list, allowing the Lean termination checker to accept them without decreasing_by. If this turns out to be infeasible, document why with a comment.
References
- Observed by AI code review on PR #9
- See CLAUDE.md termination discipline
- 主要语言
- Lean
- 星标
- 2
- 派生
- 1
- PR 合并指标
- 30 天内没有已合并 PR
贡献指南
这个仓库没有索引到贡献指南
从这里开始
- 先读完整个 Issue，再读项目的贡献指南。
- 在 Issue 下留言说明你要接手 —— 这能避免两个人做同样的事。
- Fork 仓库，在一个分支上完成修改。
- 提交 Pull Request，并在描述里引用这个 Issue 编号。
lambdaclass/lambda_compiler_kit 的其他 Issue
-
难度 1/5 1 小时以内 新手友好度 72/100
-
难度 1/5 1 小时以内 新手友好度 68/100
-
难度 2/5 1-3 小时 新手友好度 68/100
-
enhancement
难度 4/5 3-5 天 新手友好度 48/100
-
难度 2/5 1-3 小时 新手友好度 50/100
查看 lambdaclass/lambda_compiler_kit 的全部 Issue
相似的 Issue
-
难度 2/5 1-3 小时 新手友好度 75/100
JakeChampion/lang#10213 ·
-
enhancement good first issue needs testing
难度 2/5 1-3 小时 新手友好度 75/100
-
bug
难度 2/5 1-3 小时 新手友好度 75/100
bradcypert/plum#58 ·
-
flang:fir-hlfir
难度 2/5 1-3 小时 新手友好度 70/100
llvm/llvm-project#225935 ·
-
area:cards hand-tail ready-for-agent
难度 2/5 1-3 小时 新手友好度 65/100
fil-donadoni/tolaria#4446 ·