Implementa un reloj que maneje horas sin fechas.
Debes poder sumarle y restarle minutos.
Dos relojes que representen la misma hora deben ser iguales entre sí.
Para completar este ejercicio necesitas definir el tipo de dato Clock, agregar una instancia de BEq y una de ToString, e implementar las funciones:
create, que recibe dos enteros, posiblemente negativos, que representan horas y minutos respectivamente, y que crea un Clock válido.add, que recibe un Clock y una cantidad de minutos que se suman al tiempo del Clock, y que genera un nuevo Clock.subtract, que recibe un Clock y una cantidad de minutos que se restan del tiempo del Clock, y que genera un nuevo Clock.Ten en cuenta que el tipo Clock representa un reloj de 24 horas que va de «00:00» a «23:59».
Ten en cuenta que tanto las horas como los minutos de un Clock están acotados:
0 <= hour < 240 <= minute < 60En Lean es idiomático representar este tipo de restricciones a nivel de los tipos, de modo que los valores inválidos sean irrepresentables. Sin embargo, esto también requiere demostrar que un valor dado cumple con estas restricciones.
Si te animas, aquí tienes una buena introducción a este tema:
Regístrate en Exercism para aprender y dominar Lean con 100 ejercicios y mentoría humana real, todo gratis.