Implementiere eine Uhr, die Uhrzeiten ohne Datum verarbeitet.
Du solltest Minuten zu ihr addieren und von ihr subtrahieren können.
Zwei Uhren, die dieselbe Zeit darstellen, sollten gleich sein.
Um diese Übung abzuschließen, musst du den Datentyp Clock definieren, eine BEq- und eine ToString-Instanz hinzufügen und die folgenden Funktionen implementieren:
create: nimmt zwei Ganzzahlen entgegen, die auch negativ sein können und für Stunden bzw. Minuten stehen, und erzeugt eine gültige Clock.add: nimmt eine Clock und eine Anzahl Minuten entgegen, die zur Zeit der Clock addiert werden, und erzeugt eine neue Clock.subtract: nimmt eine Clock und eine Anzahl Minuten entgegen, die von der Zeit der Clock subtrahiert werden, und erzeugt eine neue Clock.Beachte, dass der Typ Clock eine 24-Stunden-Uhr darstellt, die von „00:00“ bis „23:59“ läuft.
Beachte, dass sowohl die Stunden als auch die Minuten in einer Clock beschränkt sind:
0 <= hour < 240 <= minute < 60In Lean ist es idiomatisch, solche Einschränkungen auf Typebene darzustellen, sodass ungültige Werte nicht darstellbar sind. Das erfordert allerdings auch den Beweis, dass ein gegebener Wert diese Einschränkungen erfüllt.
Wenn du dich dem gewachsen fühlst, hier eine gute Einführung in dieses Thema:
Melde dich bei Exercism an, um Lean mit 100 Übungen und echtem menschlichen Mentoring zu lernen und zu meistern, alles kostenlos.