binary and octal number notations
Nessuno ha ancora preso questa issue.
Valutazione
- Difficoltà
- 5/5
- Tempo stimato
- Più di una settimana
- Idoneità per principianti
- 35/100
- Tipo di issue
- Funzionalità
- Chiarezza
- Abbastanza chiara
- Stato di attività
- Ferma
- Ambito
- compilers
Direzione di ricerca
L’issue non indica file, test o punti di ingresso. Inizia individuando il codice esistente per il parsing e la stampa dei valori esadecimali, quindi esamina DecimalFacts e HexadecimalFacts e le relative dimostrazioni. Il lavoro è completo quando sono supportate le costanti binarie e ottali e i fatti condivisi possono coprire tutti i sistemi di numerazione senza rompere il comportamento esadecimale esistente.
Scritto dal modello di indicizzazione a partire dal testo della issue.
Descrizione
I think it would be nice to support printing and parsing of binary and octal constants in addition to hexadecimal ones. In addition it might make sense to factor out DecimalFacts and HexadecimalFacts to be parameterized over, say,
digits : Type
all_digits : list digits
digit_index : digits -> nat
all_digits_complete : forall d, List.nth_error all_digits (digit_index d) = Some d
all_digits_unique : forall n d, List.nth_error all_digits n = Some d -> digit_index d = n
and then to have proofs about list digits. This should allow compact proofs for all base systems.
cc @proux01, what do you think?
- Lingua principale
- Rocq Prover
- Stelle
- 42
- Fork
- 40
- Merge medio
- 20h 23m
- PR unite (30g)
- 2
Preparare l'ambiente
- Nessun Dockerfile né file Docker Compose
- Ha un modello di pull request
- Leggi la guida per i contributori
Come iniziare
- Leggi tutta la issue e poi la guida ai contributi del progetto.
- Commenta sulla issue per dire che te ne occupi tu — evita che due persone facciano lo stesso lavoro.
- Fai un fork del repository e lavora su un branch.
- Apri una pull request che faccia riferimento al numero della issue.
Altre issue di rocq-prover/stdlib
-
incl_dec and NoDup_dec should be Defined and not QedForse di nuovo libera Una pull request per questa issue è stata chiusa senza essere unita. Aperta
Difficoltà 1/5 1-3 ore Idoneità per principianti 65/100
rocq-prover/stdlib#25 ·
-
Reals: escape-window separation engine for the constructive Cauchy reals (abstract irrationality criterion)Forse già presa Una pull request collegata a questa issue è aperta o già unita. Aperta
Difficoltà 5/5 Più di una settimana Idoneità per principianti 35/100
rocq-prover/stdlib#312 ·
-
Maintaining NaryFunctionsAperta
Difficoltà 5/5 Più di una settimana Idoneità per principianti 25/100
rocq-prover/stdlib#293 ·
-
`QArith`: Add more rounding modes to complement `Qfloor` and `Qceiling`Forse già presa @RyanGlScott l’ha presa 88 giorni fa. Aperta
Difficoltà 3/5 1-2 giorni Idoneità per principianti 52/100
rocq-prover/stdlib#283 · 2 commenti ·
-
Inconsistent OPAM packaging of rocq-stdlibForse già presa Una pull request collegata a questa issue è aperta o già unita. Aperta
Difficoltà 4/5 3-5 giorni Idoneità per principianti 42/100
rocq-prover/stdlib#256 · 4 commenti · 3 reazioni ·
Tutte le issue di rocq-prover/stdlib
Issue simili
-
Difficoltà 2/5 1-3 ore Idoneità per principianti 74/100
I maintainer di solito rispondono entro 1 giorno
-
Difficoltà 2/5 1-3 ore Idoneità per principianti 82/100
-
Difficoltà 2/5 1-3 ore Idoneità per principianti 72/100
handsontable/hyperformula#1803 ·
I maintainer di solito rispondono entro 1 giorno
-
compile: jv_mem_calloc assertion abort after "too many function parameters" error in a nested functionForse già presa Una pull request collegata a questa issue è aperta o già unita. Aperta
Difficoltà 2/5 1-3 ore Idoneità per principianti 72/100
I maintainer di solito rispondono entro 1 giorno
-
Default-import note suggests `import * as process` for velt:process, which does not name the builtinAperta
Difficoltà 2/5 1-3 ore Idoneità per principianti 72/100
I maintainer di solito rispondono entro 1 giorno