Υλοποίησε ένα ρολόι που διαχειρίζεται ώρες χωρίς ημερομηνίες.
Θα πρέπει να μπορείς να προσθέτεις και να αφαιρείς λεπτά από αυτό.
Δύο ρολόγια που δείχνουν την ίδια ώρα θα πρέπει να είναι ίσα μεταξύ τους.
Για να ολοκληρώσεις αυτή την άσκηση, πρέπει να ορίσεις τον τύπο δεδομένων Clock, να προσθέσεις ένα στιγμιότυπο BEq και ένα στιγμιότυπο ToString, και να υλοποιήσεις τις συναρτήσεις:
create, που παίρνει δύο ακέραιους, ενδεχομένως αρνητικούς, που αντιπροσωπεύουν ώρες και λεπτά αντίστοιχα, και δημιουργεί ένα έγκυρο Clock.add, που παίρνει ένα Clock και έναν αριθμό λεπτών που θα προστεθούν στην ώρα του Clock, δημιουργώντας ένα νέο Clock.subtract, που παίρνει ένα Clock και έναν αριθμό λεπτών που θα αφαιρεθούν από την ώρα του Clock, δημιουργώντας ένα νέο Clock.Σημείωσε ότι ο τύπος Clock αντιπροσωπεύει ένα ρολόι 24 ωρών που πηγαίνει από "00:00" έως "23:59".
Σημείωσε ότι τόσο οι ώρες όσο και τα λεπτά σε ένα Clock έχουν όρια:
0 <= hour < 240 <= minute < 60Είναι ιδιωματικό στη Lean να αναπαριστάς τέτοιους περιορισμούς στο επίπεδο του τύπου, ώστε οι μη έγκυρες τιμές να είναι μη αναπαραστάσιμες. Ωστόσο, αυτό απαιτεί επίσης να αποδείξεις ότι μια δεδομένη τιμή ικανοποιεί αυτούς τους περιορισμούς.
Αν έχεις διάθεση, εδώ είναι μια καλή εισαγωγή σε αυτό το θέμα:
Γράψου στο Exercism για να μάθεις και να κατακτήσεις Lean με 100 ασκήσεις και πραγματική καθοδήγηση από ανθρώπους, όλα δωρεάν.