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

Organize examples with native_decide lint disabled

Aperta
#12 0 commenti 0 reazioni 0 assegnatari Vedi su GitHub

Nessuno ha ancora preso questa issue.

Valutazione

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

Direzione di ricerca

Inizia con CharCorrectness.lean e controlla come sono organizzate le sue dimostrazioni e i suoi esempi. Esegui il refactoring del file in modo che alla fine compaia una sezione dedicata Examples, con native_decide lint disabilitato al suo interno; mantieni i teoremi e il codice della libreria principale al di fuori di essa. Controlla gli altri file delle dimostrazioni per verificare lo stesso schema man mano che gli esempi aumentano.

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

Descrizione

Summary

Create a dedicated section Examples in each proofs file to contain example assertions that use native_decide without triggering the linter.style.nativeDecide lint that applies to the rest of the codebase.

Approach

Use section with lint option disabled:

  • Theorems and core library code remain strict (no native_decide)
  • Examples use native_decide for quick verification without linter noise
  • Clear signal about code intent and verification guarantees

Files to refactor

  • CharCorrectness.lean
  • (other proof files as they accumulate examples)

Notes

  • Place examples section at end of file
  • Examples should be non-library assertions only
  • Theorems stay outside this section and use traditional proofs
Lingua principale
Lean
Stelle
2
Fork
1
Nessuna PR unita negli ultimi 30g

Guida per i contributori

Nessuna guida per i contributori indicizzata per questo repository

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 lambdaclass/lambda_compiler_kit

Tutte le issue di lambdaclass/lambda_compiler_kit

Issue simili

Altre issue su Compilers

Ricevi le nuove issue nella tua casella

Un breve riepilogo di issue GitHub adatte ai principianti.