Implementa un orologio che gestisce orari senza date.
Dovresti poter aggiungere e sottrarre minuti.
Due orologi che rappresentano lo stesso orario devono essere uguali tra loro.
Per completare questo esercizio devi definire il tipo di dato Clock, aggiungere un'istanza di BEq e una di ToString, e implementare le funzioni:
create, che prende due numeri interi, eventualmente negativi, che rappresentano rispettivamente le ore e i minuti, e crea un Clock valido.add, che prende un Clock e un numero di minuti da aggiungere all'ora indicata nel Clock, generando un nuovo Clock.subtract, che prende un Clock e un numero di minuti da sottrarre all'ora indicata nel Clock, generando un nuovo Clock.Tieni presente che il tipo Clock rappresenta un orologio a 24 ore che va da «00:00» a «23:59».
Nota che sia le ore sia i minuti in un Clock hanno dei limiti:
0 <= hour < 240 <= minute < 60In Lean è idiomatico rappresentare questi vincoli a livello di tipo, in modo che i valori non validi siano irrappresentabili. Tuttavia, questo richiede anche di dimostrare che un dato valore soddisfa questi vincoli.
Se te la senti, ecco una buona introduzione a questo argomento:
Iscriviti a Exercism per imparare e padroneggiare Lean con 100 esercizi e il mentoring di persone reali, tutto gratis.