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

Convert to proleptic Gregorian calendar.

Equations

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

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

Convert from proleptic Gregorian calendar.

Equations

• Time.fromGregorianDate dt = let dy := Time.monthAndDayToDayOfYear (Time.isLeapYear dt.Year) ↑dt.Month.val ↑dt.Day.val; Time.fromOrdinalDayOfYear dt.Year dy

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

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

Equations

• Time.fromGregorian year month day = let dy := Time.monthAndDayToDayOfYear (Time.isLeapYear year) month day; Time.fromOrdinalDayOfYear year dy

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

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

Equations

• Time.fromGregorianValid year month day = do let day ← Time.monthAndDayToDayOfYearValid (Time.isLeapYear year) month day Time.fromOrdinalDateValid year ↑day.val

def Time.Gregorian.monthLength (year : Int) (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.fromGregorian 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.fromGregorian 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 : Time.Day) (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 : Time.Day) (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.