Hacktoberfest 2026: le issue che i maintainer hanno segnato per ottobre, aperte e adatte ai principianti. Sfoglia le issue Hacktoberfest

Naming conventions broken (cos/sin)

Aperta
#35 2 commenti 0 reazioni 0 assegnatari Vedi su GitHub

Nessuno ha ancora preso questa issue.

Valutazione

Difficoltà
2/5
Tempo stimato
1-3 ore
Idoneità per principianti
45/100
Tipo di issue
Refactoring
Chiarezza
Abbastanza chiara
Stato di attività
Ferma

Direzione di ricerca

Inizia in theories/Reals/Rtrigo_calc.v intorno alle righe 181–193 e esamina i nomi esistenti dei lemmi cos/sin confrontandoli con le forme richieste cos_3PI4 e sin_3PI4. Decidi se la compatibilità richiede alias o una ridenominazione, quindi conferma che la convenzione di denominazione sia stata affrontata senza lasciare irrisolta la questione di API esistente nell’issue.

Scritto dal modello di indicizzazione a partire dal testo della issue.

Descrizione

What happened to the naming conventions here? (These should be cos_3PI4 and sin_3PI4.)

Would the right fix be to add underscores (and potentially break things) or add aliases to the same lemmas with underscores?

https://github.com/coq/coq/blob/d886dff0857702fc4524779980ee6b7e9688c1d4/theories/Reals/Rtrigo_calc.v#L181-L193

Lingua principale
Rocq Prover
Stelle
42
Fork
40
Merge medio
20h 23m
PR unite (30g)
2

Preparare l'ambiente

Come iniziare

  1. Leggi tutta la issue e poi la guida ai contributi del progetto.
  2. Commenta sulla issue per dire che te ne occupi tu — evita che due persone facciano lo stesso lavoro.
  3. Fai un fork del repository e lavora su un branch.
  4. Apri una pull request che faccia riferimento al numero della issue.

Altre issue di rocq-prover/stdlib

Tutte le issue di rocq-prover/stdlib

Issue simili

Altre issue su DevTools

Ricevi le nuove issue nella tua casella

Un breve riepilogo di issue GitHub adatte ai principianti.