Hacktoberfest 2026: những issue maintainer đã đánh dấu cho tháng Mười, đang mở và phù hợp người mới. Xem issue Hacktoberfest

Avoiding manual conversion step & autocompletion

Đang mở
#2 0 bình luận 0 reaction 0 người được giao Xem trên GitHub

Chưa có ai nhận issue này.

Đánh giá

Độ khó
5/5
Thời gian dự kiến
Hơn một tuần
Mức phù hợp với người mới
25/100
Loại issue
Tính năng
Độ rõ ràng
Cần làm rõ
Mức độ hoạt động
Đình trệ
Lĩnh vực
cli

Hướng nghiên cứu

Bắt đầu bằng cách đọc API hiện tại của thư viện liên quan đến các giá trị Parsed, các macro cấu hình và bước chuyển đổi cuối cùng. Xác định hoàn thành là một cấu trúc đầu ra type-safe loại bỏ bước chuyển đổi bổ sung và thêm tính năng tự động hoàn thành, nhưng issue không nêu tên các tệp hoặc các bài kiểm thử cần chạy.

Do mô hình lập chỉ mục viết ra từ nội dung của issue.

Mô tả

enhancement

When I have time to work on this again (in ~2 months), I'd like to adjust the API so that no extra conversion step is necessary at the end and work on autocompletion.

For the former, a macro approach could work well, where a type-safe output structure is generated either from a Parsed value or even directly at the start using the configuration macro. The library does not really track the real type right now, so the latter should be safer.

Ngôn ngữ chính
Lean
Star
120
Fork
30
Merge trung bình
5 phút
Pull request đã merge (30 ngày)
4

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

  1. Đọc hết issue, rồi đọc hướng dẫn đóng góp của dự án.
  2. 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.
  3. Fork repository và làm thay đổi trên một nhánh.
  4. Mở pull request có tham chiếu số hiệu của issue.

Issue khác của leanprover/lean4-cli

Tất cả issue của leanprover/lean4-cli

Issue tương tự

Thêm issue về CLI

Nhận issue mới trong hộp thư của bạn

Bản tóm tắt ngắn những issue GitHub phù hợp với người mới.