leanprover-community/mathlib4

Turn `compute_degree` into a simproc

Open

#22 219 ouverte le 23 févr. 2025

Voir sur GitHub
 (3 commentaires) (1 réaction) (0 assignés)Lean (1 381 forks)github user discovery
good first issuet-meta

Métriques du dépôt

Stars
 (3 405 stars)
Métriques de merge PR
 (Métriques PR en attente)

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.

Guide contributeur

Direction de recherche
Explorez le mécanisme simproc dans Lean 4 et réimplémentez compute degree en tant que simproc, en comparant l'expérience utilisateur.
Stack technique
Aucun
Domaine
developer experience
Type d'issue
Refactorisation
DifficultéDifficulté estimée pour un nouveau contributeur, de 1 pour un très petit changement à 5 pour un travail expert.
2
Temps estiméFourchette de temps approximative pour investiguer, implémenter, tester et préparer une pull request.
Une demi journée
Statut d'activitéDisponibilité apparente de l'issue : fraîche, active, ancienne, bloquée ou en attente d'un mainteneur.
Active
ClartéClarté avec laquelle l'issue explique le changement attendu, les critères d'acceptation et la prochaine étape.
Claire
Prérequis
Lean
Accessibilité débutantScore de 1 à 100 estimant l'accessibilité de cette issue pour un premier contributeur.
30