Implementa um relógio que lida com horas, sem datas.
Deves conseguir adicionar e subtrair minutos ao relógio.
Dois relógios que representam a mesma hora devem ser iguais entre si.
Para completar este exercício, tens de definir o tipo de dados Clock, adicionar uma instância de BEq e de ToString, e implementar as funções:
create, que recebe dois inteiros, possivelmente negativos, que representam as horas e os minutos, respetivamente, e cria um Clock válido.add, que recebe um Clock e um número de minutos a adicionar ao tempo do Clock, gerando um novo Clock.subtract, que recebe um Clock e um número de minutos a subtrair ao tempo do Clock, gerando um novo Clock.Repara que o tipo Clock representa um relógio de 24 horas, que vai de "00:00" a "23:59".
Repara que tanto as horas como os minutos de um Clock têm limites:
0 <= hour < 240 <= minute < 60É idiomático em Lean representar estas restrições ao nível dos tipos, para que valores inválidos sejam irrepresentáveis. No entanto, isso também exige provar que um determinado valor satisfaz estas restrições.
Se te sentires à altura, aqui está uma boa introdução a este tópico:
Inscreve-te no Exercism para aprenderes e dominares Lean com 100 exercícios, e mentoria humana real, tudo grátis.