電阻色碼

說明

如果你想用 Raspberry Pi 打造一些東西，大概會用到_電阻_。在這個練習中，你需要知道關於電阻的兩件事：

• 每個電阻都有一個電阻值。
• 電阻很小，小到如果直接把電阻值印在上面的話，會很難閱讀。

為了解決這個問題，製造商會在電阻上印上顏色色帶，用來表示它們的電阻值。每個色帶都有所在的位置和一個數值。

電阻的前 2 個色帶採用簡單的編碼方式：每種顏色都對應到單一數字。

在這個練習中，你會建立一個實用的程式，這樣就不必記住每個色帶的數值了。

這些顏色的編碼如下：

• black: 0
• brown: 1
• red: 2
• orange: 3
• yellow: 4
• green: 5
• blue: 6
• violet: 7
• grey: 8
• white: 9

這個練習的目標，是建立一種方式，用來：

• 查詢特定色帶所對應的數字值
• 列出各種不同的色帶顏色

記憶口訣能把顏色對應到數字，而這些數字以陣列儲存時，剛好會對應到它們在陣列中的索引：Better Be Right Or Your Great Big Values Go Wrong.

關於電阻顏色編碼的更多資訊，可以在維基百科的 Electronic color code 條目找到。

定義語法

在這道練習中，你必須使用c*前綴來定義顏色的語法，例如c*black。根據說明，這個語法應該在編譯期展開成每個顏色對應的值，型別為Fin 10。同樣地，你必須使用c*all定義一個包含所有顏色值的陣列語法。

這項任務很可能需要你使用 notation 或 macro。你可以參考這份參考資料。

因為新語法是在編譯期展開，除非所有必要的語法都已定義，否則任何測試都無法通過編譯。因此，我們不依賴傳統的執行期測試，而是使用定理來檢查所有的值。如果一個定理通過型別檢查，你就可以把它視為通過的測試。

如果你在本機工作，或是在 Lean 的線上遊樂場中工作，就能透過 Lean InfoView 立即得知每個定理成功或失敗，以及失敗的原因。

---

出處

Maud de Vries, Erik Schierboom