rocq-prover/stdlib

Le issue su cui forse qualcuno sta già lavorando sono in fondo alla lista. Ordina tutto per data

• Maintaining NaryFunctions

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 5/5 Più di una settimana Idoneità per principianti 25/100

  rocq-prover/stdlib#293 · Aperta il 15/7/2026

• deprecating List.nth in favor of List.nth_default

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 5/5 Più di una settimana Idoneità per principianti 25/100

  rocq-prover/stdlib#243 · Aperta il 4/3/2026

• Importing PeanoNat.Nat shadows eq definition

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 5/5 Più di una settimana Idoneità per principianti 25/100

  rocq-prover/stdlib#242 · 3 commenti · Aperta il 2/3/2026

• Documentation could be automatically deployed

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 2/5 1-3 ore Idoneità per principianti 25/100

  rocq-prover/stdlib#241 · Aperta il 23/2/2026

• Releasing? (Docker CI images do not support latest stdlib)

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 4/5 3-5 giorni Idoneità per principianti 35/100

  rocq-prover/stdlib#230 · 11 commenti · Aperta il 28/1/2026

• Using dune when installing the package

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 4/5 3-5 giorni Idoneità per principianti 42/100

  rocq-prover/stdlib#225 · 2 commenti · Aperta il 14/11/2025

• Regression: Importing ZArith leads to setoid_rewrite performance degradation

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 4/5 3-5 giorni Idoneità per principianti 42/100

  rocq-prover/stdlib#200 · 2 commenti · Aperta il 23/7/2025

• same html title for all files (stdlib doc)

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 3/5 1-2 giorni Idoneità per principianti 42/100

  rocq-prover/stdlib#195 · 2 commenti · Aperta il 17/7/2025

• Github CI anomaly zoo

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 4/5 3-5 giorni Idoneità per principianti 25/100

  rocq-prover/stdlib#168 · 4 commenti · Aperta il 7/6/2025

• Design: connecting booleans to their meaning

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 5/5 Più di una settimana Idoneità per principianti 25/100

  rocq-prover/stdlib#165 · 1 reazione · Aperta il 5/6/2025

• GitHub CI queuing

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 4/5 3-5 giorni Idoneità per principianti 25/100

  rocq-prover/stdlib#153 · 10 commenti · Aperta il 31/5/2025

• Require status checks to pass before merging (for auto-merge, no policy change)

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 4/5 3-5 giorni Idoneità per principianti 30/100

  rocq-prover/stdlib#148 · 3 commenti · Aperta il 13/5/2025

• CI: is there a way to see CI-built HTML documentation for an unmerged PR?

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 4/5 3-5 giorni Idoneità per principianti 25/100

  rocq-prover/stdlib#145 · 1 commento · Aperta il 10/5/2025

• CI jobs should explicitly set the `name` field

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 2/5 1-3 ore Idoneità per principianti 55/100

  rocq-prover/stdlib#142 · Aperta il 6/5/2025

• "Cachix setup coq" failed on CI

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 3/5 1-2 giorni Idoneità per principianti 25/100

  rocq-prover/stdlib#140 · Aperta il 4/5/2025

• `NoDup_dec` definition is opaque

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 1/5 Meno di un'ora Idoneità per principianti 50/100

  rocq-prover/stdlib#125 · Aperta il 31/3/2025

• What is the merging policy for stdlib? (contributing.md is nonsense)

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 4/5 3-5 giorni Idoneità per principianti 35/100

  rocq-prover/stdlib#116 · 2 commenti · Aperta il 3/3/2025

• Keep All.v in topological order

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 3/5 1-2 giorni Idoneità per principianti 42/100

  rocq-prover/stdlib#106 · 1 commento · Aperta il 12/2/2025

• `int64` equivalent for `ExtrOcamlIntConv`

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 5/5 Più di una settimana Idoneità per principianti 25/100

  rocq-prover/stdlib#3 · Aperta il 21/12/2024

• stdlib exports conflicting notations

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 4/5 3-5 giorni Idoneità per principianti 35/100

  rocq-prover/stdlib#4 · Aperta il 20/12/2024

• Confusing warning: Using Vector.t is known to be technically difficult

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 3/5 1-2 giorni Idoneità per principianti 35/100

  rocq-prover/stdlib#5 · 5 commenti · Aperta il 7/12/2024

• ZifyBool overriding zify_post_hook is a bad idea

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 4/5 3-5 giorni Idoneità per principianti 25/100

  rocq-prover/stdlib#6 · Aperta il 5/6/2024

• Hard to fix Stdlib arithmetic deprecations in 8.18 breaking many projects in 8.19

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 5/5 Più di una settimana Idoneità per principianti 25/100

  rocq-prover/stdlib#7 · 18 commenti · Aperta il 3/1/2024

• `Scheme Equality for nat` + `Require Import Coq.Logic.Eqdep_dec.` breaks `inversion` ("Illegal application" at Qed)

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 5/5 Più di una settimana Idoneità per principianti 25/100

  rocq-prover/stdlib#8 · Aperta il 2/10/2023

• Bottlenecks in standard library

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 4/5 3-5 giorni Idoneità per principianti 35/100

  rocq-prover/stdlib#9 · 1 commento · Aperta il 20/7/2023

• List.rev is unexpectedly quadratic

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 1/5 Meno di un'ora Idoneità per principianti 35/100

  rocq-prover/stdlib#10 · 3 commenti · Aperta il 12/7/2023

• `ListNotations` breaks primitive array syntax

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 3/5 1-2 giorni Idoneità per principianti 35/100

  rocq-prover/stdlib#11 · 8 commenti · Aperta il 5/7/2023

• Import Nsatz redefines "0" and "1"

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 4/5 3-5 giorni Idoneità per principianti 35/100

  rocq-prover/stdlib#12 · 6 commenti · Aperta il 29/5/2023

• Missing lemmas about Prop: absorbing or neutral elements for various operations

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 2/5 1-3 ore Idoneità per principianti 45/100

  rocq-prover/stdlib#14 · 3 commenti · Aperta il 14/12/2022

• Setoid rewriting hardcodes stdlib paths instead of relying on Register

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 4/5 3-5 giorni Idoneità per principianti 35/100

  rocq-prover/stdlib#15 · 1 commento · Aperta il 24/11/2022

• Conflicting use of "~=" in Coq.Program.Equality and Coq.Structures.Equalities

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 3/5 1-2 giorni Idoneità per principianti 35/100

  rocq-prover/stdlib#16 · Aperta il 31/7/2022

• coqc infinite loop in type class resolution

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 4/5 3-5 giorni Idoneità per principianti 35/100

  rocq-prover/stdlib#17 · 8 commenti · Aperta il 20/6/2022

• The Standard Library should not be adding transitivity and symmetry hints to `core`

  Forse di nuovo libera Una pull request per questa issue è stata chiusa senza essere unita. Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 4/5 3-5 giorni Idoneità per principianti 38/100

  rocq-prover/stdlib#18 · 3 commenti · Aperta il 3/6/2022

• Dep_elim database not used?

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 4/5 3-5 giorni Idoneità per principianti 35/100

  rocq-prover/stdlib#20 · 1 commento · Aperta il 19/5/2022

• `Require Import Coq.Sorting.Permutation.` slows down `rewrite_strat` > 10x

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 4/5 3-5 giorni Idoneità per principianti 35/100

  rocq-prover/stdlib#21 · 7 commenti · Aperta il 17/2/2022

• Strong natural induction should be simpler

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 3/5 1-2 giorni Idoneità per principianti 45/100

  rocq-prover/stdlib#22 · 1 reazione · Aperta il 10/8/2021

• binary and octal number notations

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 5/5 Più di una settimana Idoneità per principianti 35/100

  rocq-prover/stdlib#23 · 1 commento · 1 reazione · Aperta il 6/5/2021

• Cannot pattern match on exist in program definitions

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 5/5 Più di una settimana Idoneità per principianti 25/100

  rocq-prover/stdlib#24 · Aperta il 23/4/2021

• incl_dec and NoDup_dec should be Defined and not Qed

  Forse di nuovo libera Una pull request per questa issue è stata chiusa senza essere unita. Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 1/5 1-3 ore Idoneità per principianti 65/100

  rocq-prover/stdlib#25 · Aperta il 21/4/2021

• btauto should not modify core HintDb

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 5/5 Più di una settimana Idoneità per principianti 25/100

  rocq-prover/stdlib#27 · 4 commenti · Aperta il 14/7/2020

• definition of field and ring theories excluded from standard library reference main page

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 2/5 1-3 ore Idoneità per principianti 35/100

  rocq-prover/stdlib#28 · 3 commenti · 1 reazione · Aperta il 16/4/2020

• Require Import Int63 breaks `Definition land := ...`

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 5/5 Più di una settimana Idoneità per principianti 20/100

  rocq-prover/stdlib#29 · 1 commento · 1 reazione · Aperta il 25/3/2020

• NoDup List Cut Function

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 4/5 3-5 giorni Idoneità per principianti 35/100

  rocq-prover/stdlib#30 · 1 commento · Aperta il 28/2/2020

• Z.mod_mul_r and Z.rem_mul_r reversed

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 2/5 1-3 ore Idoneità per principianti 45/100

  rocq-prover/stdlib#31 · Aperta il 30/10/2019

• Reals: Make "Rsqr x" and an alias for "x^2"

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 5/5 Più di una settimana Idoneità per principianti 25/100

  rocq-prover/stdlib#32 · 17 commenti · Aperta il 1/9/2019

• ExtrOCamlInt63 contains an upper-case C in its name

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 2/5 1-3 ore Idoneità per principianti 45/100

  rocq-prover/stdlib#33 · 10 commenti · Aperta il 26/8/2019

• suprirsing hints leak

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 3/5 1-2 giorni Idoneità per principianti 35/100

  rocq-prover/stdlib#34 · 4 commenti · Aperta il 26/7/2019

• Naming conventions broken (cos/sin)

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 2/5 1-3 ore Idoneità per principianti 45/100

  rocq-prover/stdlib#35 · 2 commenti · Aperta il 8/7/2019

• Please add gprogress and grepeat and gtry and g+ and g[> tac.. ]

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 5/5 Più di una settimana Idoneità per principianti 20/100

  rocq-prover/stdlib#37 · 2 commenti · 1 reazione · Aperta il 8/3/2019

• Declare `Hint Mode` for `Reflexive`, `Symmetric`, `Equivalence`, ...

  Aperta

  ⋯Segnala un problema con questa issue

  • Qualcosa non va?

  • Già presa in carico
  • Non adatta ai principianti
  • Obsoleta o non valida
  • Altro…
  • Invia Annulla

  Difficoltà 2/5 1-3 ore Idoneità per principianti 38/100

  rocq-prover/stdlib#38 · 9 commenti · Aperta il 30/1/2019