Reloj

Reloj

Media

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 datos Clock, añadir una instancia de BEq y otra de ToString, e implementar las funciones:

  • create, que recibe dos números enteros, posiblemente negativos, que representan las horas y los minutos respectivamente, y crea un Clock válido.
  • add, que recibe un Clock y un número de minutos que se suman a la hora del Clock, y genera un Clock nuevo.
  • subtract, que recibe un Clock y un número de minutos que se restan de la hora del Clock, y genera un Clock nuevo.

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 tipo, de modo que los valores no válidos sean irrepresentables. Sin embargo, esto también requiere demostrar que un valor dado cumple estas restricciones.

Si te ves con ganas, 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 pestaña nueva
Lean Exercism

¿Listo para empezar Reloj?

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