Time package
Port of the haskell time library to Lean 4 (WIP).
Missing modules
Usage
see time library doc
From Haskell to Lean
Take the function toOrdinalDate, which computes the ISO 8601 ordinal date given a modified Julian day.
In Haskell toOrdinalDate has the type
type Year = Integer
type DayOfYear = Int
toOrdinalDate :: Day -> (Year, DayOfYear)
and computes the year and the day of year.
In Lean toOrdinalDate has the type
inductive DayOfYear where
| common : Time.Icc 1 365 -> DayOfYear
| leap : Time.Icc 1 366 -> DayOfYear
structure OrdinalDate where
year : Int
dayOfYear : DayOfYear
isValid : match dayOfYear with
| .common _ => isLeapYear year = false
| .leap _ => isLeapYear year = true
def toOrdinalDate : Day → OrdinalDate
and computes the year and the day of year and gives a proof that ordinal date is a valid date.
Build
- update: lake update
- build: lake build
- build docs: lake -R -Kenv=dev update && lake -R -Kenv=dev build Time:docs