leanprover-community/mathlib4

Turn `compute_degree` into a simproc

Open

#22,219 opened on Feb 23, 2025

View on 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)

Description

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.

Contributor guide

Research direction
Explore the simproc mechanism in Lean 4 and reimplement compute degree as a simproc, comparing user experience.
Tech stack
None
Domain
developer experience
Issue type
Refactor
DifficultyEstimated implementation difficulty for a new contributor, from 1 for very small changes to 5 for expert-level work.
2
Estimated timeA rough time range for an experienced contributor to investigate, implement, test, and prepare a pull request.
Half day
Activity statusHow available the issue appears right now: fresh, active, stale, blocked, or waiting on maintainer input.
Active
ClarityHow clearly the issue explains the expected change, acceptance criteria, and next step.
Clear
Prerequisites
Lean
Newbie friendlinessA 1-100 score estimating how approachable this issue is for first-time contributors.
30