Вказівки
Якщо ми хочемо щось зібрати на 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 одразу отримаємо зворотний звʼязок про те, чи кожна теорема успішна, чи ні, і чому вона не проходить.
