Anleitung
Wenn du etwas mit einem Raspberry Pi bauen willst, wirst du wahrscheinlich Widerstände verwenden.
Für diese Übung musst du zwei Dinge über sie wissen:
- Jeder Widerstand hat einen Widerstandswert.
- Widerstände sind klein. So klein, dass es schwer zu lesen wäre, wenn du den Widerstandswert darauf drucken würdest.
Um dieses Problem zu umgehen, drucken Hersteller farbcodierte Ringe auf die Widerstände, die ihren Widerstandswert angeben.
Jeder Ring hat eine Position und einen numerischen Wert.
Die ersten beiden Ringe eines Widerstands folgen einem einfachen Kodierungsschema: Jede Farbe steht für eine einzelne Zahl.
In dieser Übung schreibst du ein hilfreiches Programm, damit du dir die Werte der Ringe nicht merken musst.
Diese Farben sind wie folgt kodiert:
- black: 0
- brown: 1
- red: 2
- orange: 3
- yellow: 4
- green: 5
- blue: 6
- violet: 7
- grey: 8
- white: 9
Das Ziel dieser Übung ist es, eine Möglichkeit zu schaffen:
- den numerischen Wert nachzuschlagen, der zu einem bestimmten Farbring gehört
- die verschiedenen Farben der Ringe aufzulisten
Eselsbrücken ordnen den Farben die Zahlen zu, die, als Array gespeichert, zufällig auf ihren Index im Array abbilden:
Better Be Right Or Your Great Big Values Go Wrong.
Mehr Informationen zur Farbkodierung von Widerständen findest du im Wikipedia-Artikel zum Farbcode für elektronische Bauteile.
Syntax definieren
In dieser Übung musst du Syntax für Farben mit dem c*-Präfix definieren, z. B. c*black.
Diese Syntax sollte zur Kompilierzeit zum entsprechenden Wert jeder Farbe als Fin 10 expandieren, gemäß den Anweisungen.
Ebenso musst du Syntax für ein Array aller Farbwerte mit c*all definieren.
Diese Aufgabe erfordert wahrscheinlich, dass du entweder Notationen oder Makros verwendest.
Vielleicht möchtest du einen Blick in die Referenz werfen.
Weil neue Syntax zur Kompilierzeit expandiert wird, würde kein Test kompilieren, es sei denn, die gesamte erforderliche Syntax definiert ist.
Aus diesem Grund überprüfen wir alle Werte mit Theoremen, anstatt uns auf traditionelle Laufzeittests zu verlassen.
Wenn ein Theorem die Typprüfung besteht, kannst du es als bestandenen Test betrachten.
Wenn du lokal oder im Online-Playground von Lean arbeitest, bekommst du über Lean InfoView sofortiges Feedback darüber, ob ein Theorem erfolgreich ist oder fehlschlägt, und warum es fehlschlägt.
