抵抗器カラー

説明

Raspberry Piを使って何かを作りたいなら、おそらく_抵抗器_を使うでしょう。 この演習では、抵抗器について2つのことを知っておく必要があります：

• それぞれの抵抗器には抵抗値があります。
• 抵抗器はとても小さく、抵抗値を印刷しても読み取るのが難しいほどです。

この問題を解決するために、メーカーは抵抗器に色分けされた帯を印刷し、抵抗値を表しています。 それぞれの帯には、位置と数値があります。

抵抗器の最初の2つの帯には、簡単な符号化方式があります。それぞれの色は1つの数値に対応します。

この演習では、帯の値を覚えなくて済むように、便利なプログラムを作ります。

これらの色は次のように符号化されています：

• 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.

抵抗器のカラーコードについての詳細は、電子色コードのWikipedia記事を参照してください。

構文の定義

この演習では、c*という接頭辞を使って色の構文を定義する必要があります。たとえばc*blackです。 この構文は、説明にあるとおり、コンパイル時に各色に対応する値をFin 10として展開するものでなければなりません。 同じように、c*allを使って、すべての色の値からなる配列の構文も定義する必要があります。

この課題では、記法かマクロのどちらかを使うことになるでしょう。 リファレンスを確認するとよいかもしれません。

新しい構文はコンパイル時に展開されるため、必要な構文がすべて定義されていないと、どのテストもコンパイルに失敗します。 そのため、従来の実行時テストに頼る代わりに、すべての値を定理を使って確認します。 定理の型チェックが通れば、それは合格したテストだと考えてよいでしょう。

ローカルで作業する場合も、Leanのオンラインプレイグラウンドを使う場合も、Lean InfoViewを通じて、どの定理が成功したか失敗したか、そしてなぜ失敗したかをすぐに確認できます。

---

出典

Maud de Vries, Erik Schierboom