Istruzioni
Se vuoi costruire qualcosa con un Raspberry Pi, probabilmente userai dei resistori.
Per questo esercizio devi sapere due cose sul loro conto:
- Ogni resistore ha un valore di resistenza.
- I resistori sono piccoli, così piccoli che se ci stampassi sopra il valore di resistenza sarebbe difficile da leggere.
Per aggirare questo problema, i produttori stampano sui resistori delle bande colorate che indicano il loro valore di resistenza.
Ogni banda ha una posizione e un valore numerico.
Le prime 2 bande di un resistore seguono un semplice schema di codifica: ogni colore corrisponde a un singolo numero.
In questo esercizio creerai un programma utile, così non dovrai ricordarti i valori delle bande.
Questi colori sono codificati come segue:
- black: 0
- brown: 1
- red: 2
- orange: 3
- yellow: 4
- green: 5
- blue: 6
- violet: 7
- grey: 8
- white: 9
L'obiettivo di questo esercizio è creare un modo per:
- cercare il valore numerico associato a una particolare banda colorata
- elencare i diversi colori delle bande
Le tecniche mnemoniche associano i colori ai numeri che, quando vengono memorizzati in un array, finiscono per corrispondere al loro indice nell'array:
Better Be Right Or Your Great Big Values Go Wrong.
Puoi trovare maggiori informazioni sulla codifica dei colori dei resistori nell'articolo di Wikipedia sul codice dei colori elettronico.
Definire la sintassi
In questo esercizio, dovrai definire una sintassi per i colori usando il prefisso c*, ad esempio c*black.
Questa sintassi dovrebbe espandersi in fase di compilazione nel valore corrispondente di ogni colore come Fin 10, come indicato nelle istruzioni.
Allo stesso modo, dovrai definire una sintassi per un array con tutti i valori dei colori usando c*all.
Questo compito richiederà probabilmente di usare notazioni o macro.
Potresti dare un'occhiata a un riferimento.
Dato che la nuova sintassi viene espansa in fase di compilazione, qualsiasi test non riuscirebbe a compilarsi se non fosse definita tutta la sintassi richiesta.
Per questo motivo, invece di affidarci ai tradizionali test a runtime, controlliamo tutti i valori usando i teoremi.
Se un teorema supera il controllo dei tipi, puoi considerarlo un test superato.
Se lavori in locale o nel playground online di Lean, riceverai un feedback immediato, tramite Lean InfoView, su se un teorema riesce o fallisce e sul perché fallisce.
