Introdução
A forma como medimos o tempo é meio bagunçada.
Temos 60 segundos em um minuto e 60 minutos em uma hora.
Isso vem da antiga Babilônia, onde o 60 era a base do sistema numérico deles.
Temos 24 horas em um dia, 7 dias em uma semana, e quantos dias em um mês?
Bem, a quantidade de dias em um mês depende não só de qual mês é, mas também do tipo de calendário usado no país em que você vive.
E se, em vez disso, usássemos apenas segundos para expressar intervalos de tempo?
Aí podemos usar os prefixos do sistema métrico para escrever grandes quantidades de segundos em valores mais fáceis de compreender.
- Uma receita pode explicar que você precisa deixar os brownies assarem no forno por dois quilosegundos (ou seja, dois mil segundos).
- Talvez você e sua família viajassem para algum lugar exótico por dois megasegundos (ou seja, dois milhões de segundos).
- E se você e seu cônjuge estivessem casados há um bilhão de segundos, vocês comemorariam um gigasegundo de casados.
Se algum dia colonizarmos Marte ou algum outro planeta, medir o tempo vai ficar ainda mais bagunçado.
Quando alguém diz "ano", está falando de um ano na Terra ou de um ano em Marte?
A ideia deste exercício veio do romance de ficção científica "A Deepness in the Sky", do autor Vernor Vinge.
Nele, o autor usa o sistema métrico como base para medir o tempo.
Instruções
Sua tarefa é determinar a data e a hora um gigassegundo depois de uma certa data.
Um gigassegundo é um bilhão de segundos.
Ou seja, um 1 seguido de nove zeros.
Se você nasceu em 24 de janeiro de 2015 às 22:00 (10:00:00pm), você completaria um gigassegundo de vida em 2 de outubro de 2046 às 23:46:40 (11:46:40pm).
Datas e horas
O Lean tem suporte a datas e horas no módulo Time da biblioteca padrão.
Esse módulo precisa ser importado no início do arquivo:
import Std.Time
Datas e horas em Lean são fortemente tipadas: cada componente (ano, mês, dia, hora, etc.) tem seu próprio tipo e precisa ser construído explicitamente.
Existem várias macros no módulo Time que podem ajudar nessa tarefa.
