leanprover-community/mathlib4

Turn `compute_degree` into a simproc

Open

#22.219 aberto em 23 de fev. de 2025

Ver no GitHub
 (3 comments) (1 reaction) (0 assignees)Lean (1.381 forks)github user discovery
good first issuet-meta

Métricas do repositório

Stars
 (3.405 stars)
Métricas de merge de PR
 (Métricas PR pendentes)

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.

Guia do colaborador

Direção de pesquisa
Explore o mecanismo simproc no Lean 4 e reimplemente compute degree como um simproc, comparando a experiência do usuário.
Pilha de tecnologia
None
Domain
developer experience
Tipo Issue
Refatoração
DifficultyDificuldade de implementação estimada para um novo contribuidor, de 1 para alterações muito pequenas a 5 para trabalho de nível especializado.
2
Tempo estimadoUm intervalo de tempo aproximado para um colaborador experiente investigar, implementar, testar e preparar um pull request.
Meio dia
Status da atividadeQuão disponível o issue aparece agora: novo, ativo, obsoleto, bloqueado ou aguardando entrada do mantenedor.
Ativo
ClarityCom que clareza o issue explica a mudança esperada, os critérios de aceitação e a próxima etapa.
Claro
Prerequisites
Lean
Simpatia para novatosUma pontuação de 1 a 100 que estima o quão acessível este issue é para colaboradores iniciantes.
30