Introduction
La façon dont on mesure le temps est un peu chaotique.
Il y a 60 secondes dans une minute, et 60 minutes dans une heure.
Cela remonte à l'ancienne Babylone, où l'on utilisait 60 comme base de son système de numération.
Il y a 24 heures dans une journée, 7 jours dans une semaine, et combien de jours dans un mois ?
Eh bien, cela dépend non seulement du mois, mais aussi du type de calendrier utilisé dans le pays où tu vis.
Et si, au lieu de ça, on n'utilisait que des secondes pour exprimer les intervalles de temps ?
On pourrait alors utiliser les préfixes du système métrique pour écrire de grands nombres de secondes sous forme de quantités plus faciles à appréhender.
- Une recette de cuisine peut expliquer qu'il faut laisser les brownies cuire au four pendant deux kilosecondes (soit deux mille secondes).
- Tu partirais peut-être avec ta famille vers un endroit exotique pendant deux mégasecondes (soit deux millions de secondes).
- Et si tu étais marié à ton conjoint depuis mille millions de secondes, tu fêterais ton anniversaire d'une gigaseconde.
Si un jour on colonise Mars ou une autre planète, mesurer le temps deviendra encore plus compliqué.
Si quelqu'un dit « année », parle-t-il d'une année sur Terre ou d'une année sur Mars ?
L'idée de cet exercice vient du roman de science-fiction "A Deepness in the Sky" de l'auteur Vernor Vinge.
L'auteur y utilise le système métrique comme base pour mesurer le temps.
Instructions
Ta tâche consiste à déterminer la date et l'heure une gigaseconde après une date donnée.
Une gigaseconde correspond à un milliard de secondes.
C'est un 1 suivi de neuf zéros.
Si tu étais né le 24 janvier 2015 à 22 h 00, tu atteindrais l'âge d'une gigaseconde le 2 octobre 2046 à 23 h 46 min 40 s.
Dates et heures
Lean prend en charge les dates et les heures dans le module Time de la bibliothèque standard.
Il faut l'importer au début du fichier :
import Std.Time
Les dates et les heures en Lean sont fortement typées : chaque composant (année, mois, jour, heure, etc.) a son propre type et doit être construit explicitement.
Le module Time contient un certain nombre de macros qui peuvent t'aider dans cette tâche.
