style: proof style improvements in RegexSpec.lean
Chưa có ai nhận issue này.
Đánh giá
- Độ khó
- 4/5
- Thời gian dự kiến
- 3-5 ngày
- Mức phù hợp với người mới
- 35/100
- Loại issue
- Tái cấu trúc
- Độ rõ ràng
- Khá rõ ràng
- Mức độ hoạt động
- Đình trệ
- Lĩnh vực
- compilers
Hướng nghiên cứu
Đọc RegexSpec.lean, bắt đầu với regex_match_sound và các chứng minh Glushkov, sau đó so sánh các bổ đề chuyên biệt với các bổ đề tổng quát trong Matcher.lean. Xem lại các nhánh DecidableEq và binding dr bị loại bỏ; công việc được hoàn thành khi các chú thích, các trường hợp chứng minh mạnh mẽ và việc tái sử dụng các bổ đề tổng quát được áp dụng mà không thay đổi hành vi của chứng minh.
Do mô hình lập chỉ mục viết ra từ nội dung của issue.
Mô tả
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
- Ngôn ngữ chính
- Lean
- Star
- 2
- Fork
- 1
- Chỉ số merge pull request
- Không có pull request nào được merge trong 30 ngày
Hướng dẫn đóng góp
Chưa lập chỉ mục được hướng dẫn đóng góp cho kho mã nguồn này
Bắt đầu từ đâu
- Đọc hết issue, rồi đọc hướng dẫn đóng góp của dự án.
- Bình luận trên issue rằng bạn sẽ nhận — tránh hai người làm cùng một việc.
- Fork repository và làm thay đổi trên một nhánh.
- Mở pull request có tham chiếu số hiệu của issue.
Issue khác của lambdaclass/lambda_compiler_kit
-
Độ khó 1/5 Dưới một giờ Mức phù hợp với người mới 72/100
-
Độ khó 1/5 Dưới một giờ Mức phù hợp với người mới 68/100
-
Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 68/100
-
enhancement
Độ khó 4/5 3-5 ngày Mức phù hợp với người mới 48/100
-
Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 50/100
Tất cả issue của lambdaclass/lambda_compiler_kit
Issue tương tự
-
Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 75/100
objectionary/eo#8923 ·
-
Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 75/100
-
Coarray integration tests carry no LABELS, so run_tests.py silently skips them under every backend Đang mởcoarray
Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 70/100
-
Độ khó 2/5 1-3 giờ Mức phù hợp với người mới 75/100
-
internal.h中，漏掉了1个定义。 Đang mở
Độ khó 1/5 Dưới một giờ Mức phù hợp với người mới 95/100