structure Std.Time.PlainDate : Type

PlainDate represents a date in the Year-Month-Day (YMD) format. It encapsulates the year, month, and day components, with validation to ensure the date is valid.

• year : Year.Offset

  The year component of the date. It is represented as an Offset type from Year.

• month : Month.Ordinal

  The month component of the date. It is represented as an Ordinal type from Month.

• day : Day.Ordinal

  The day component of the date. It is represented as an Ordinal type from Day.

• valid : self.year.Valid self.month self.day

  Validates the date by ensuring that the year, month, and day form a correct and valid date.

theorem Std.Time.PlainDate.ext {x y : PlainDate} (year : x.year = y.year) (month : x.month = y.month) (day : x.day = y.day) : x = y

theorem Std.Time.PlainDate.ext_iff {x y : PlainDate} : x = y ↔ x.year = y.year ∧ x.month = y.month ∧ x.day = y.day

@[instance_reducible]

instance Std.Time.instReprPlainDate : Repr PlainDate

Equations

• Std.Time.instReprPlainDate = { reprPrec := Std.Time.instReprPlainDate.repr }

def Std.Time.instReprPlainDate.repr : PlainDate → Nat → Std.Format

Equations

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

@[instance_reducible]

instance Std.Time.instDecidableEqPlainDate : DecidableEq PlainDate

Equations

• Std.Time.instDecidableEqPlainDate = Std.Time.instDecidableEqPlainDate.decEq

def Std.Time.instDecidableEqPlainDate.decEq (x✝ x✝¹ : PlainDate) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Std.Time.instInhabitedPlainDate : Inhabited PlainDate

Equations

• Std.Time.instInhabitedPlainDate = { default := { year := 1, month := 1, day := 1, valid := Std.Time.instInhabitedPlainDate._proof_1 } }

@[instance_reducible]

instance Std.Time.instOrdPlainDate : Ord PlainDate

Equations

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

theorem Std.Time.PlainDate.compare_def : compare = compareLex (compareOn fun (x : PlainDate) => x.year) (compareLex (compareOn fun (x : PlainDate) => x.month) (compareOn fun (x : PlainDate) => x.day))

instance Std.Time.instTransOrdPlainDate : TransOrd PlainDate

instance Std.Time.instLawfulEqOrdPlainDate : LawfulEqOrd PlainDate

@[inline]

def Std.Time.PlainDate.ofYearMonthDayClip (year : Year.Offset) (month : Month.Ordinal) (day : Day.Ordinal) : PlainDate

Creates a PlainDate by clipping the day to ensure validity. This function forces the date to be valid by adjusting the day to fit within the valid range to fit the given month and year.

Equations

• Std.Time.PlainDate.ofYearMonthDayClip year month day = { year := year, month := month, day := Std.Time.Month.Ordinal.clipDay year.isLeap month day, valid := ⋯ }

@[instance_reducible]

instance Std.Time.PlainDate.instInhabited : Inhabited PlainDate

Equations

• Std.Time.PlainDate.instInhabited = { default := { year := 0, month := 1, day := 1, valid := Std.Time.PlainDate.instInhabited._proof_1 } }

@[inline]

def Std.Time.PlainDate.ofYearMonthDay? (year : Year.Offset) (month : Month.Ordinal) (day : Day.Ordinal) : Option PlainDate

Creates a new PlainDate from year, month, and day components.

Equations

• Std.Time.PlainDate.ofYearMonthDay? year month day = if valid : year.Valid month day then some { year := year, month := month, day := day, valid := valid } else none

@[inline]

def Std.Time.PlainDate.ofYearOrdinal (year : Year.Offset) (ordinal : Day.Ordinal.OfYear year.isLeap) : PlainDate

Creates a PlainDate from a year and a day ordinal within that year.

Equations

• Std.Time.PlainDate.ofYearOrdinal year ordinal = match Std.Time.ValidDate.ofOrdinal ordinal with | ⟨(month, day), proof⟩ => { year := year, month := month, day := day, valid := proof }

def Std.Time.PlainDate.ofEpochDay (day : Day.Offset) : PlainDate

Creates a PlainDate from the number of days since January 1st, 1970.

Equations

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

def Std.Time.PlainDate.alignedWeekOfMonth (date : PlainDate) : Week.Aligned.Ordinal

Returns the aligned week of the month for a PlainDate. Weeks are fixed 7-day slots starting from day 1: days 1–7 are week 1, days 8–14 are week 2, etc.

Equations

• date.alignedWeekOfMonth = ((Std.Time.Internal.Bounded.LE.sub date.day 1).ediv 7 Std.Time.PlainDate.alignedWeekOfMonth._proof_1✝).add 1

def Std.Time.PlainDate.quarter (date : PlainDate) : Internal.Bounded.LE 1 4

Determines the quarter of the year for the given PlainDate.

Equations

• date.quarter = ((Std.Time.Internal.Bounded.LE.sub date.month 1).ediv 3 Std.Time.PlainDate.quarter._proof_1✝).add 1

def Std.Time.PlainDate.dayOfYear (date : PlainDate) : Day.Ordinal.OfYear date.year.isLeap

Transforms a PlainDate into a Day.Ordinal.OfYear.

Equations

• date.dayOfYear = Std.Time.ValidDate.dayOfYear ⟨(date.month, date.day), ⋯⟩

@[inline]

def Std.Time.PlainDate.era (date : PlainDate) : Year.Era

Determines the era of the given PlainDate based on its year.

Equations

• date.era = date.year.era

@[inline]

def Std.Time.PlainDate.inLeapYear (date : PlainDate) : Bool

Checks if the PlainDate is in a leap year.

Equations

• date.inLeapYear = date.year.isLeap

def Std.Time.PlainDate.toEpochDay (date : PlainDate) : Day.Offset

Converts a PlainDate to the number of days since 1970-01-01T00:00:00.

Equations

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

@[inline]

def Std.Time.PlainDate.addDays (date : PlainDate) (days : Day.Offset) : PlainDate

Adds a given number of days to a PlainDate.

Equations

• date.addDays days = Std.Time.PlainDate.ofEpochDay (date.toEpochDay + days)

@[inline]

def Std.Time.PlainDate.subDays (date : PlainDate) (days : Day.Offset) : PlainDate

Subtracts a given number of days from a PlainDate.

Equations

• date.subDays days = date.addDays (-days)

@[inline]

def Std.Time.PlainDate.addWeeks (date : PlainDate) (weeks : Week.Offset) : PlainDate

Adds a given number of weeks to a PlainDate.

Equations

• date.addWeeks weeks = Std.Time.PlainDate.ofEpochDay (date.toEpochDay + weeks.toDays)

@[inline]

def Std.Time.PlainDate.subWeeks (date : PlainDate) (weeks : Week.Offset) : PlainDate

Subtracts a given number of weeks from a PlainDate.

Equations

• date.subWeeks weeks = date.addWeeks (-weeks)

def Std.Time.PlainDate.addMonthsClip (date : PlainDate) (months : Month.Offset) : PlainDate

Adds a given number of months to a PlainDate, clipping the day to the last valid day of the month.

Equations

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

@[inline]

def Std.Time.PlainDate.subMonthsClip (date : PlainDate) (months : Month.Offset) : PlainDate

Subtracts Month.Offset from a PlainDate, it clips the day to the last valid day of that month.

Equations

• date.subMonthsClip months = date.addMonthsClip (-months)

def Std.Time.PlainDate.rollOver (year : Year.Offset) (month : Month.Ordinal) (day : Day.Ordinal) : PlainDate

Creates a PlainDate by rolling over the extra days to the next month.

Equations

• Std.Time.PlainDate.rollOver year month day = (Std.Time.PlainDate.ofYearMonthDayClip year month 1).addDays (day.toOffset - 1)

@[inline]

def Std.Time.PlainDate.withYearClip (dt : PlainDate) (year : Year.Offset) : PlainDate

Creates a new PlainDate by adjusting the year to the given year value. The month and day remain unchanged, and any invalid days for the new year will be handled according to the clip behavior.

Equations

• dt.withYearClip year = Std.Time.PlainDate.ofYearMonthDayClip year dt.month dt.day

@[inline]

def Std.Time.PlainDate.withYearRollOver (dt : PlainDate) (year : Year.Offset) : PlainDate

Creates a new PlainDate by adjusting the year to the given year value. The month and day are rolled over to the next valid month and day if necessary.

Equations

• dt.withYearRollOver year = Std.Time.PlainDate.rollOver year dt.month dt.day

def Std.Time.PlainDate.addMonthsRollOver (date : PlainDate) (months : Month.Offset) : PlainDate

Adds a given number of months to a PlainDate, rolling over any excess days into the following month.

Equations

• date.addMonthsRollOver months = ((Std.Time.PlainDate.ofYearMonthDayClip date.year date.month 1).addMonthsClip months).addDays (date.day.toOffset - 1)

@[inline]

def Std.Time.PlainDate.subMonthsRollOver (date : PlainDate) (months : Month.Offset) : PlainDate

Subtracts Month.Offset from a PlainDate, rolling over excess days as needed.

Equations

• date.subMonthsRollOver months = date.addMonthsRollOver (-months)

@[inline]

def Std.Time.PlainDate.addYearsRollOver (date : PlainDate) (years : Year.Offset) : PlainDate

Adds Year.Offset to a PlainDate, rolling over excess days to the next month, or next year.

Equations

• date.addYearsRollOver years = date.addMonthsRollOver (Int.mul years 12)

@[inline]

def Std.Time.PlainDate.subYearsRollOver (date : PlainDate) (years : Year.Offset) : PlainDate

Subtracts Year.Offset from a PlainDate, rolling over excess days to the next month.

Equations

• date.subYearsRollOver years = date.addMonthsRollOver (-Int.mul years 12)

@[inline]

def Std.Time.PlainDate.addYearsClip (date : PlainDate) (years : Year.Offset) : PlainDate

Adds Year.Offset to a PlainDate, clipping the day to the last valid day of the month.

Equations

• date.addYearsClip years = date.addMonthsClip (Int.mul years 12)

@[inline]

def Std.Time.PlainDate.subYearsClip (date : PlainDate) (years : Year.Offset) : PlainDate

Subtracts Year.Offset from a PlainDate, clipping the day to the last valid day of the month.

Equations

• date.subYearsClip years = date.addMonthsClip (-Int.mul years 12)

@[inline]

def Std.Time.PlainDate.withDaysClip (dt : PlainDate) (days : Day.Ordinal) : PlainDate

Creates a new PlainDate by adjusting the day of the month to the given days value, with any out-of-range days clipped to the nearest valid date.

Equations

• dt.withDaysClip days = Std.Time.PlainDate.ofYearMonthDayClip dt.year dt.month days

@[inline]

def Std.Time.PlainDate.withDaysRollOver (dt : PlainDate) (days : Day.Ordinal) : PlainDate

Creates a new PlainDate by adjusting the day of the month to the given days value, with any out-of-range days rolled over to the next month or year as needed.

Equations

• dt.withDaysRollOver days = Std.Time.PlainDate.rollOver dt.year dt.month days

@[inline]

def Std.Time.PlainDate.withMonthClip (dt : PlainDate) (month : Month.Ordinal) : PlainDate

Creates a new PlainDate by adjusting the month to the given month value. The day remains unchanged, and any invalid days for the new month will be handled according to the clip behavior.

Equations

• dt.withMonthClip month = Std.Time.PlainDate.ofYearMonthDayClip dt.year month dt.day

@[inline]

def Std.Time.PlainDate.withMonthRollOver (dt : PlainDate) (month : Month.Ordinal) : PlainDate

Creates a new PlainDate by adjusting the month to the given month value. The day is rolled over to the next valid month if necessary.

Equations

• dt.withMonthRollOver month = Std.Time.PlainDate.rollOver dt.year month dt.day

def Std.Time.PlainDate.weekday (date : PlainDate) : Weekday

Calculates the Weekday of a given PlainDate using Zeller's Congruence for the Gregorian calendar.

Equations

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

def Std.Time.PlainDate.weekOfMonth (date : PlainDate) (firstDay : Weekday := Weekday.monday) : Week.Ordinal

Returns the week of the month for the given PlainDate, where weeks start on firstDay. The first partial week containing day 1 is week 1, so weeks may span fewer than 7 days.

Equations

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

def Std.Time.PlainDate.withWeekday (date : PlainDate) (desiredWeekday : Weekday) : PlainDate

Sets the date to the specified desiredWeekday. If the desiredWeekday is the same as the current weekday, the original date is returned without modification. If the desiredWeekday is in the future, the function adjusts the date forward to the next occurrence of that weekday.

Equations

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

def Std.Time.PlainDate.startOfWeekBasedYear (year : Year.Offset) (firstDay : Weekday) (minimalDays : Internal.Bounded.LE 0 6) : PlainDate

Returns the first day of the week-based year for the given year, where weeks start on firstDay and the first week must contain at least minimalDays days of the new year.

Equations

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

def Std.Time.PlainDate.weekOfYear (date : PlainDate) (firstDay : Weekday := Weekday.monday) (minDaysBounded : Internal.Bounded.LE 0 6 := Internal.Bounded.LE.mk 4 weekOfYear._proof_1) : Week.OfYear.Ordinal

Returns the week number within the week-based year for the given PlainDate, using firstDay as the start of the week and minDays as the minimum number of days required in the first week of the year (default 4 for ISO 8601). Dates before the first week of the calendar year are counted as part of the last week of the previous year.

Equations

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

def Std.Time.PlainDate.weekYear (date : PlainDate) (firstDay : Weekday := Weekday.monday) (minDays : Internal.Bounded.LE 0 6 := Internal.Bounded.LE.mk 4 weekOfYear._proof_1) : Year.Offset

Returns the week-based year for the given PlainDate, using firstDay as the start of the week and minDays as the minimum number of days in the first week of the year (default 4 for ISO 8601).

Equations

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

@[instance_reducible]

instance Std.Time.PlainDate.instHAddOffset : HAdd PlainDate Day.Offset PlainDate

Equations

• Std.Time.PlainDate.instHAddOffset = { hAdd := Std.Time.PlainDate.addDays }

@[instance_reducible]

instance Std.Time.PlainDate.instHSubOffset : HSub PlainDate Day.Offset PlainDate

Equations

• Std.Time.PlainDate.instHSubOffset = { hSub := Std.Time.PlainDate.subDays }

@[instance_reducible]

instance Std.Time.PlainDate.instHAddOffset_1 : HAdd PlainDate Week.Offset PlainDate

Equations

• Std.Time.PlainDate.instHAddOffset_1 = { hAdd := Std.Time.PlainDate.addWeeks }

@[instance_reducible]

instance Std.Time.PlainDate.instHSubOffset_1 : HSub PlainDate Week.Offset PlainDate

Equations

• Std.Time.PlainDate.instHSubOffset_1 = { hSub := Std.Time.PlainDate.subWeeks }