Implemente um relógio que lida com horários sem datas.
Você deve conseguir somar e subtrair minutos a ele.
Dois relógios que representam o mesmo horário devem ser iguais entre si.
Para completar este exercício, você precisa definir o tipo de dado Clock, adicionar uma instância de BEq e uma de ToString, e implementar as funções:
create, que recebe dois inteiros, possivelmente negativos, representando horas e minutos, respectivamente, e cria um Clock válido.add, que recebe um Clock e um número de minutos a serem somados ao horário do Clock, gerando um novo Clock.subtract, que recebe um Clock e um número de minutos a serem subtraídos do horário do Clock, gerando um novo Clock.Note que o tipo Clock representa um relógio de 24 horas, que vai de "00:00" a "23:59".
Note que tanto as horas quanto os minutos em um Clock são limitados:
0 <= hour < 240 <= minute < 60É idiomático em Lean representar essas restrições no nível do tipo, de modo que valores inválidos sejam irrepresentáveis. No entanto, isso também exige provar que um dado valor satisfaz essas restrições.
Se você estiver disposto, aqui está uma boa introdução a este tópico:
Crie sua conta no Exercism para aprender e dominar Lean com 100 exercícios e mentoria humana de verdade, tudo de graça.