Time package

Port of the haskell time library to Lean 4 (WIP).

Missing modules


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.


  • update: lake update
  • build: lake build
  • build docs: lake -R -Kenv=dev update && lake -R -Kenv=dev build Time:docs