Εισαγωγή
Ο τρόπος που μετράμε τον χρόνο είναι λίγο μπερδεμένος.
Έχουμε 60 δευτερόλεπτα στο λεπτό και 60 λεπτά στην ώρα.
Αυτό προέρχεται από την αρχαία Βαβυλώνα, όπου χρησιμοποιούσαν το 60 ως βάση του αριθμητικού τους συστήματος.
Μια μέρα έχει 24 ώρες, μια εβδομάδα έχει 7 μέρες, και πόσες μέρες έχει ένας μήνας;
Λοιπόν, ο αριθμός των ημερών σε έναν μήνα δεν εξαρτάται μόνο από το ποιος μήνας είναι, αλλά και από το είδος του ημερολογίου που χρησιμοποιείται στη χώρα όπου ζεις.
Τι θα γινόταν όμως αν χρησιμοποιούσαμε μόνο δευτερόλεπτα για να εκφράζουμε χρονικά διαστήματα;
Τότε θα μπορούσαμε να χρησιμοποιήσουμε τα προθέματα του μετρικού συστήματος για να γράφουμε μεγάλους αριθμούς δευτερολέπτων σε ποσότητες πιο εύκολα κατανοητές.
- Μια συνταγή μπορεί να σου πει να αφήσεις τα μπράουνις να ψηθούν στον φούρνο για δύο κιλοδευτερόλεπτα (δηλαδή δύο χιλιάδες δευτερόλεπτα).
- Ίσως εσύ και η οικογένειά σου να ταξιδεύατε κάπου εξωτικά για δύο μεγαδευτερόλεπτα (δηλαδή δύο εκατομμύρια δευτερόλεπτα).
- Και αν εσύ και ο σύντροφός σου ήσασταν παντρεμένοι για χίλια εκατομμύρια δευτερόλεπτα, θα γιορτάζατε την επέτειό σας του ενός γιγαδευτερολέπτου.
Αν ποτέ αποικίσουμε τον Άρη ή κάποιον άλλο πλανήτη, η μέτρηση του χρόνου θα γίνει ακόμα πιο μπερδεμένη.
Αν κάποιος πει "έτος", εννοεί ένα έτος στη Γη ή ένα έτος στον Άρη;
Η ιδέα για αυτή την άσκηση προήλθε από το μυθιστόρημα επιστημονικής φαντασίας "A Deepness in the Sky" του συγγραφέα Vernor Vinge.
Σε αυτό, ο συγγραφέας χρησιμοποιεί το μετρικό σύστημα ως βάση για τις μετρήσεις του χρόνου.
Οδηγίες
Η αποστολή σου είναι να προσδιορίσεις την ημερομηνία και την ώρα ένα γιγαδευτερόλεπτο μετά από μια δεδομένη ημερομηνία.
Ένα γιγαδευτερόλεπτο είναι ένα δισεκατομμύριο δευτερόλεπτα.
Δηλαδή ένα 1 με εννέα μηδενικά μετά.
Αν γεννήθηκες στις 24 Ιανουαρίου 2015 στις 22:00 (10:00:00 μ.μ.), τότε θα είχες ζήσει ένα γιγαδευτερόλεπτο στις 2 Οκτωβρίου 2046 στις 23:46:40 (11:46:40 μ.μ.).
Ημερομηνίες και ώρες
Το Lean διαθέτει υποστήριξη για ημερομηνίες και ώρες στην ενότητα Time της τυπικής βιβλιοθήκης.
Πρέπει να εισαχθεί στην αρχή του αρχείου:
import Std.Time
Οι ημερομηνίες και οι ώρες στο Lean είναι ισχυρά τυποποιημένες, κάθε component (έτος, μήνας, ημέρα, ώρα κ.λπ.) έχει τον δικό του τύπο και πρέπει να κατασκευαστεί ρητά.
Υπάρχουν αρκετές μακροεντολές στην ενότητα Time που μπορούν να βοηθήσουν με αυτό το έργο.
