leanprover-community/physlib

Remove `erw`s

Aberta

#385 aberto em 10 de mar. de 2025

Ver no GitHubGuia do colaborador
 (1 comentário) (0 reação) (0 responsável)Lean (139 forks)auto 404
good first issuehelp-wanted

Métricas do repositório

Stars
 (642 estrelas)
Métricas de merge de PR
 (Métricas PR pendentes)

Description

There are lots of erw [...] in PhysLean. These are slow, and thus it is beneficial for them to be removed.

To remove an erw [...] usually means changing the corresponding lemma to simp-normal form.

Guia do colaborador

Direção de pesquisa
Pesquise no código por padrões `erw`. Para cada um, identifique o lema usado e considere se pode ser tornado em forma `simp` normal. Em seguida, substitua `erw` por `simp` ou `rw` conforme apropriado. Garanta que as alterações passem na suíte de testes.
Pilha de tecnologia
None
Domain
performance
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.
70