leanprover-community/mathlib4

Turn `compute_degree` into a simproc

Open

#22.219 aperta il 23 feb 2025

Vedi su GitHub
 (3 commenti) (1 reazione) (0 assegnatari)Lean (1381 fork)github user discovery
good first issuet-meta

Metriche repository

Star
 (3405 star)
Metriche merge PR
 (Metriche PR in attesa)

Descrizione

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.

Guida contributor

Direzione di ricerca
Esplora il meccanismo simproc in Lean 4 e reimplementa compute degree come simproc, confrontando l'esperienza utente.
Tech stack
Nessuno
Dominio
developer experience
Tipo issue
Refactoring
DifficoltàQuanto dovrebbe essere impegnativa per un nuovo contributor.
2
Tempo stimatoTempo stimato per completare e verificare uno scope piccolo.
Mezza giornata
Stato attivitàQuanto è probabile che la issue sia ancora attiva e reviewable.
Attiva
ChiarezzaQuanto chiaramente la issue descrive problema, scope e risultato atteso.
Chiara
Prerequisiti
Lean
Adatta ai principiantiQuanto la issue è adatta a contributor alla prima esperienza.
30