Instruções
Se queres construir algo com um Raspberry Pi, provavelmente vais usar resistências.
Para este exercício, precisas de saber duas coisas sobre elas:
- Cada resistência tem um valor de resistência.
- As resistências são pequenas. Tão pequenas que, se imprimisses nelas o valor de resistência, seria difícil de ler.
Para contornar este problema, os fabricantes imprimem faixas codificadas por cores nas resistências, para indicar os respetivos valores de resistência.
Cada faixa tem uma posição e um valor numérico.
As primeiras 2 faixas de uma resistência seguem um esquema de codificação simples: cada cor corresponde a um único número.
Neste exercício vais criar um programa útil para não teres de memorizar os valores das faixas.
Estas cores são codificadas da seguinte forma:
- black: 0
- brown: 1
- red: 2
- orange: 3
- yellow: 4
- green: 5
- blue: 6
- violet: 7
- grey: 8
- white: 9
O objetivo deste exercício é criar uma forma de:
- consultar o valor numérico associado a uma determinada faixa de cor
- listar as diferentes cores das faixas
As mnemónicas associam as cores aos números que, quando guardados num array, acabam por corresponder ao seu índice nesse array:
Better Be Right Or Your Great Big Values Go Wrong.
Podes encontrar mais informação sobre a codificação de cores das resistências no artigo da Wikipédia sobre o código de cores eletrónico.
Definir sintaxe
Neste exercício, tens de definir sintaxe para as cores usando o prefixo c*, por exemplo, c*black.
Esta sintaxe deve expandir-se em tempo de compilação para o valor correspondente de cada cor como um Fin 10, de acordo com as instruções.
Da mesma forma, tens de definir sintaxe para um array com todos os valores das cores usando c*all.
Esta tarefa vai provavelmente exigir que uses notações ou macros.
Podes querer consultar uma referência.
Como a nova sintaxe é expandida em tempo de compilação, qualquer teste falharia a compilação se não estivesse definida toda a sintaxe necessária.
Por este motivo, em vez de nos apoiarmos nos tradicionais testes em tempo de execução, verificamos todos os valores através de teoremas.
Se um teorema passar a verificação de tipos, podes considerá-lo um teste bem-sucedido.
Se trabalhares localmente ou no playground online do Lean, vais receber feedback imediato sobre se um teorema tem sucesso ou falha, e porque falha, através do InfoView do Lean.
