Uhr

Uhr

Mittel

Anleitung

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.

Implementierung

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.

Advanced

Beachte, dass sowohl die Stunden als auch die Minuten in einer Clock beschränkt sind:

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

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


Quelle

Pairing-Session mit Erin Drummond
Über GitHub bearbeiten Der Link öffnet sich in einem neuen Fenster oder Tab
Lean Exercism

Bereit, mit Uhr zu starten?

Melde dich bei Exercism an, um Lean mit 100 Übungen und echtem menschlichen Mentoring zu lernen und zu meistern, alles kostenlos.