leanprover-community/mathlib4

Turn `compute_degree` into a simproc

Open

#22,219 opened on 2025年2月23日

GitHub で見る
 (3 comments) (1 reaction) (0 assignees)Lean (1,381 forks)github user discovery
good first issuet-meta

Repository metrics

Stars
 (3,405 stars)
PR merge metrics
 (PR metrics pending)

説明

compute_degree is a prime example of a piece of meta code that could be implemented as a simproc. It would be interesting to reimplement it as such and compare the user experience.

コントリビューターガイド

調査方針
Lean 4 の simproc メカニズムを調査し、compute degree を simproc として再実装し、ユーザーエクスペリエンスを比較します。
技術スタック
なし
領域
developer experience
Issue 種別
リファクタリング
難度新しい貢献者にとっての実装難度です。1 は非常に小さな変更、5 は専門的な作業です。
2
推定時間経験ある貢献者が調査、実装、テスト、pull request 準備にかけるおおよその時間範囲です。
半日
活動状況Issue が今どれだけ取り組みやすいかを示します。新しい、活発、古い、ブロック中、またはメンテナー入力待ちなどです。
アクティブ
明確さ期待される変更、受け入れ条件、次の手順がどれだけ明確かを示します。
明確
前提条件
Lean
初心者向け度初回貢献者にどれだけ取り組みやすいかを 1-100 で推定したスコアです。
30