Introdução
A forma como medimos o tempo é um bocado confusa.
Um minuto tem 60 segundos e uma hora tem 60 minutos.
Isto vem da antiga Babilónia, onde o 60 era a base do sistema de numeração.
Um dia tem 24 horas, uma semana tem 7 dias, e quantos dias tem um mês?
Bom, o número de dias de um mês depende não só do mês em questão, mas também do tipo de calendário usado no país onde vives.
E se, em vez disso, usássemos apenas segundos para expressar intervalos de tempo?
Assim, podemos usar os prefixos do sistema métrico para escrever grandes números de segundos em quantidades mais fáceis de compreender.
- Uma receita pode explicar que tens de deixar os brownies no forno durante dois quilosegundos (ou seja, dois mil segundos).
- Talvez tu e a tua família viajassem até um lugar exótico durante dois megassegundos (ou seja, dois milhões de segundos).
- E se tu e o teu cônjuge estivessem casados há mil milhões de segundos, celebrariam o vosso aniversário de um gigassegundo.
Se algum dia colonizarmos Marte ou outro planeta qualquer, medir o tempo vai ficar ainda mais confuso.
Quando alguém diz «ano», está a referir-se a um ano na Terra ou a um ano em Marte?
A ideia para este 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
A tua tarefa é determinar a data e a hora um gigassegundo depois de uma determinada data.
Um gigassegundo é mil milhões de segundos.
Ou seja, é o número um seguido de nove zeros.
Se tivesses nascido a 24 de janeiro de 2015, às 22:00 (10:00:00 da noite), a 2 de outubro de 2046, às 23:46:40 (11:46:40 da noite), terias um gigassegundo de idade.
Datas e horas
O Lean tem suporte para datas e horas no módulo Time da biblioteca padrão.
É preciso importá-lo no início do ficheiro:
import Std.Time
As datas e horas em Lean têm tipos fortes: cada componente (ano, mês, dia, hora, etc.) tem o seu próprio tipo e tem de ser construído explicitamente.
Há várias macros no módulo Time que te podem ajudar nesta tarefa.
