Implémente une horloge qui gère des heures sans date.
Tu dois pouvoir y ajouter des minutes et en soustraire.
Deux horloges qui représentent la même heure doivent être égales entre elles.
Pour venir à bout de cet exercice, il te faut définir le type de données Clock, ajouter une instance BEq et une instance ToString, et implémenter les fonctions :
create, qui prend deux entiers, éventuellement négatifs, représentant respectivement les heures et les minutes, et qui crée un Clock valide.add, qui prend un Clock et un nombre de minutes à ajouter à l'heure du Clock, et qui génère un nouveau Clock.subtract, qui prend un Clock et un nombre de minutes à soustraire de l'heure du Clock, et qui génère un nouveau Clock.À noter que le type Clock représente une horloge de 24 heures, allant de "00:00" à "23:59".
À noter que les heures comme les minutes d'un Clock sont bornées :
0 <= hour < 240 <= minute < 60En Lean, il est idiomatique de représenter ce genre de contraintes au niveau du type, de sorte que les valeurs invalides soient irreprésentables. Cela demande cependant de prouver qu'une valeur donnée satisfait ces contraintes.
Si le cœur t'en dit, voici une bonne introduction à ce sujet :
Inscris-toi sur Exercism pour apprendre et maîtriser Lean avec 100 exercices, et un vrai mentorat humain, le tout gratuitement.