Instruções
Se você quiser construir algo usando um Raspberry Pi, provavelmente vai usar resistores.
Para este exercício, você precisa saber duas coisas sobre eles:
- Cada resistor tem um valor de resistência.
- Resistores são pequenos. Tão pequenos que, se você imprimisse o valor da resistência neles, seria difícil de ler.
Para contornar esse problema, os fabricantes imprimem faixas codificadas por cores nos resistores para indicar seus valores de resistência.
Cada faixa tem uma posição e um valor numérico.
As duas primeiras faixas de um resistor seguem um esquema de codificação simples: cada cor corresponde a um único número.
Neste exercício, você vai criar um programa útil para não precisar decorar os valores das faixas.
Essas cores são codificadas assim:
- 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 faixa de cor específica
- listar as diferentes cores de faixa
Os mnemônicos associam as cores aos números que, quando armazenados como um array, acabam correspondendo ao índice de cada uma no array:
Better Be Right Or Your Great Big Values Go Wrong.
Mais informações sobre a codificação de cores dos resistores podem ser encontradas no artigo da Wikipédia sobre código de cores eletrônico.
Definindo a sintaxe
Neste exercício, você deve definir uma sintaxe para as cores usando o prefixo c*, por exemplo, c*black.
Essa sintaxe deve expandir, 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, você deve definir uma sintaxe para um array com todos os valores de cor usando c*all.
É provável que esta tarefa exija que você use notações ou macros.
Talvez você queira dar uma olhada em uma referência.
Como a sintaxe nova é expandida em tempo de compilação, qualquer teste falharia na compilação a menos que toda a sintaxe necessária esteja definida.
Por esse motivo, em vez de depender de testes tradicionais em tempo de execução, verificamos todos os valores usando teoremas.
Se um teorema passar na verificação de tipos, você pode considerá-lo um teste aprovado.
Se você trabalhar localmente ou no playground online do Lean, receberá feedback instantâneo, pelo Lean InfoView, sobre se cada teorema é bem-sucedido ou falha, e por que falha.
