Reals: Make "Rsqr x" and an alias for "x^2"
Nadie ha tomado este issue todavía.
Evaluación
- Dificultad
- 5/5
- Tiempo estimado
- Más de una semana
- Aptitud para principiantes
- 25/100
- Tipo de issue
- Refactorización
- Claridad
- Necesita aclaración
- Estado de actividad
- Estancado
- Área
- devtools
Línea de trabajo
Empieza revisando las definiciones de la biblioteca Reals relacionadas con Rsqr, x^2 y sqrt, y después inspecciona la field tactic y los lemas trigonométricos mencionados en el issue. Comprueba las implicaciones de rendimiento para CoqInterval antes de proponer la limpieza; para darlo por terminado se requiere acuerdo sobre la representación y un comportamiento coherente de la biblioteca.
Escrito por el modelo de indexación a partir del texto del issue.
Descripción
Some developments of the Reals library use a wild mix between Rsqr x (aka x²) and x^2. the field tactic supports (afaikt) only x^2 while most of the lemmas connecting x^2 and sqrt use Rsqr. Trigonometric lemmas use a mix of both. As a result many proofs have to convert between the two forms from time to time. Also proof search is made substantially harder by this.
I would suggest to clean this up by making Rsqr an alias for x^2. The small performance advantage given by Rsqr should not be significant and less important that cleanliness and usability of the library.
@silene, @thery : can you please comment on this, especially also on the performance implications e.g. in CoqInterval (I always used x^2 there btw.)
- Lenguaje dominante
- Rocq Prover
- Estrellas
- 45
- Forks
- 39
- Merge medio
- 4 d 12 h
- PR fusionados (30 d)
- 5
Preparar el entorno
- Sin Dockerfile ni archivo de Docker Compose
- Tiene una plantilla de pull request
- Leer la guía de contribución
Primeros pasos
- Lee el issue completo y luego la guía de contribución del proyecto.
- Comenta en el issue que vas a ocuparte — evita que dos personas hagan lo mismo.
- Haz un fork del repositorio y trabaja en una rama.
- Abre un pull request que haga referencia al número del issue.
Más de rocq-prover/stdlib
-
incl_dec and NoDup_dec should be Defined and not QedQuizá libre de nuevo Un pull request para esta issue se cerró sin fusionarse. Abierto
Dificultad 1/5 1-3 horas Aptitud para principiantes 65/100
rocq-prover/stdlib#25 ·
-
Reals: a constructive pi for the constructive Cauchy reals with a strong irrationality separation theorem (Leibniz series)Posiblemente ocupada @hy7pc8gfmf-dotcom la tomó hace 27 días. Abierto
Dificultad 5/5 Más de una semana Aptitud para principiantes 6/100
rocq-prover/stdlib#315 ·
-
Reals: escape-window separation engine for the constructive Cauchy reals (abstract irrationality criterion)Posiblemente ocupada Un pull request vinculado a esta issue está abierto o ya se fusionó. Abierto
Dificultad 5/5 Más de una semana Aptitud para principiantes 35/100
rocq-prover/stdlib#312 ·
-
Maintaining NaryFunctionsAbierto
Dificultad 5/5 Más de una semana Aptitud para principiantes 25/100
rocq-prover/stdlib#293 ·
-
Inconsistent OPAM packaging of rocq-stdlibPosiblemente ocupada Un pull request vinculado a esta issue está abierto o ya se fusionó. Abierto
Dificultad 4/5 3-5 días Aptitud para principiantes 42/100
rocq-prover/stdlib#256 · 4 comentarios · 3 reacciones ·
Todos los issues de rocq-prover/stdlib
Issues similares
-
Dificultad 2/5 1-3 horas Aptitud para principiantes 82/100
richardcase/skills#26 ·
Los mantenedores suelen responder en 1 día
-
pending close triaging
Dificultad 2/5 1-3 horas Aptitud para principiantes 82/100
anomalyco/opencode#62040 · 1 comentario ·
Los mantenedores suelen responder en 1 día
-
beginner blocked
Dificultad 2/5 1-3 horas Aptitud para principiantes 82/100
hiero-ledger/hiero-sdk-js#4670 ·
Los mantenedores suelen responder en 1 día
-
Dificultad 2/5 1-3 horas Aptitud para principiantes 72/100
nvim-tree/nvim-tree.lua#3383 ·
Los mantenedores suelen responder en 1 día
-
Skill: support MSVC debuggerAbierto
Dificultad 2/5 1-3 horas Aptitud para principiantes 68/100
Los mantenedores suelen responder en 1 día