电阻色环

说明

如果你想用 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。

关于电阻色码的更多信息，可以在电子色码维基百科条目中找到。

定义语法

在本练习中，你必须使用c*前缀来为颜色定义语法，例如c*black。 按照说明，这种语法应该在编译时展开为每种颜色对应的Fin 10值。 同样，你必须使用c*all来为包含所有颜色值的数组定义语法。

这项任务很可能需要你使用记法或宏。 你也许想查阅一篇参考文档。

由于新语法在编译时展开，只要还有必需的语法没有定义，任何测试都无法编译通过。 因此，我们不使用传统的运行时测试，而是用定理来检查所有值。 如果某个定理通过了类型检查，你就可以认为它是一项通过的测试。

如果你在本地工作，或者在 Lean 的在线演练场中工作，就可以通过 Lean InfoView 立即得知某个定理成功还是失败，以及失败的原因。

---

来源

Maud de Vries, Erik Schierboom