Reloj

Reloj

Intermedia

Instrucciones

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í.

Implementación

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».

Advanced

Ten en cuenta que tanto las horas como los minutos de un Clock están acotados:

  • 0 <= hour < 24
  • 0 <= minute < 60

En 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:


Fuente

Sesión de programación en pareja con Erin Drummond
Editar en GitHub El enlace se abre en una ventana o una pestaña nuevas
Lean Exercism

¿Todo listo para empezar Reloj?

Regístrate en Exercism para aprender y dominar Lean con 100 ejercicios y mentoría humana real, todo gratis.