def Time.toGregorian (date : Time.Day) : Time.Date

Convert to proleptic Gregorian calendar.

Equations

• Time.toGregorian date = Time.ordinalDateToDate (Time.toOrdinalDate date)

def Time.fromGregorian (dt : Time.Date) : Time.Day

Convert from proleptic Gregorian calendar.

Equations

• Time.fromGregorian dt = Time.fromOrdinalDate (Time.dateToOrdinalDate dt)

def Time.fromGregorianClipped (year month day : Int) : Time.Day

Convert from proleptic Gregorian calendar. Invalid values will be clipped to the correct range, month first, then day.

Equations

• Time.fromGregorianClipped year month day = Time.fromOrdinalDate (Time.monthAndDayToDayOfYear year month day)

def Time.fromGregorianValid (year month day : Int) : Option Time.Day

Convert from proleptic Gregorian calendar. Invalid values give result none.

Equations

• Time.fromGregorianValid year month day = do let d ← Time.monthAndDayToDayOfYearValid year month day some (Time.fromOrdinalDate d)

def Time.Gregorian.addDays (n : Int) (dt : Time.Date) : Time.Date

Equations

• Time.Gregorian.addDays n dt = Time.ordinalDateToDate (Time.OrdinalDate.addDays n (Time.dateToOrdinalDate dt))

def Time.Gregorian.monthLength (year month : Int) : Int

The number of days in a given month according to the proleptic Gregorian calendar.

Equations

• One or more equations did not get rendered due to their size.

def Time.Gregorian.addMonthsClip (n : Int) (day : Time.Day) : Time.Day

Add months, with days past the last day of the month clipped to the last day. For instance, 2005-01-30 + 1 month = 2005-02-28.

Equations

• Time.Gregorian.addMonthsClip n day = match Time.Gregorian.addMonths n day with | (y, m, d) => Time.fromGregorianClipped y m d

def Time.Gregorian.addMonthsRollOver (n : Int) (day : Time.Day) : Time.Day

Add months, with days past the last day of the month rolling over to the next month. For instance, 2005-01-30 + 1 month = 2005-03-02.

Equations

• Time.Gregorian.addMonthsRollOver n day = match Time.Gregorian.addMonths n day with | (y, m, d) => Time.Day.addDays (d - 1) (Time.fromGregorianClipped y m 1)

def Time.Gregorian.addYearsClip (n : Int) (day : Time.Day) : Time.Day

Add years, matching month and day, with Feb 29th clipped to Feb 28th if necessary. For instance, 2004-02-29 + 2 years = 2006-02-28.

Equations

• Time.Gregorian.addYearsClip n day = Time.Gregorian.addMonthsClip (n * 12) day

def Time.Gregorian.addYearsRollOver (n : Int) (day : Time.Day) : Time.Day

Add years, matching month and day, with Feb 29th rolled over to Mar 1st if necessary. -- For instance, 2004-02-29 + 2 years = 2006-03-01.

Equations

• Time.Gregorian.addYearsRollOver n day = Time.Gregorian.addMonthsRollOver (n * 12) day

def Time.Gregorian.addDurationClip (cd : Time.CalendarDiffDays) (day : Time.Day) : Time.Day

Add months (clipped to last day), then add days

Equations

• Time.Gregorian.addDurationClip cd day = Time.Day.addDays cd.days (Time.Gregorian.addMonthsClip cd.months day)

def Time.Gregorian.addDurationRollOver (cd : Time.CalendarDiffDays) (day : Time.Day) : Time.Day

Add months (rolling over to next month), then add days

Equations

• Time.Gregorian.addDurationRollOver cd day = Time.Day.addDays cd.days (Time.Gregorian.addMonthsRollOver cd.months day)

def Time.Gregorian.diffDurationClip (day2 day1 : Time.Day) : Time.CalendarDiffDays

Calendrical difference, with as many whole months as possible

Equations

• One or more equations did not get rendered due to their size.

def Time.Gregorian.diffDurationRollOver (day2 day1 : Time.Day) : Time.CalendarDiffDays

Calendrical difference, with as many whole months as possible.

Equations

• One or more equations did not get rendered due to their size.