Documentation

Std.Time.Date.PlainDate

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.

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

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

  • 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.

Instances For
    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
    @[inline]

    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
      Instances For
        @[inline]

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

        Equations
          Instances For
            @[inline]

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

            Equations
              Instances For

                Creates a PlainDate from the number of days since the UNIX epoch (January 1st, 1970).

                Equations
                  Instances For

                    Returns the unaligned week of the month for a PlainDate (day divided by 7, plus 1).

                    Equations
                      Instances For

                        Determines the quarter of the year for the given PlainDate.

                        Equations
                          Instances For

                            Transforms a PlainDate into a Day.Ordinal.OfYear.

                            Equations
                              Instances For
                                @[inline]

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

                                Equations
                                  Instances For
                                    @[inline]

                                    Checks if the PlainDate is in a leap year.

                                    Equations
                                      Instances For

                                        Converts a PlainDate to the number of days since the UNIX epoch.

                                        Equations
                                          Instances For
                                            @[inline]

                                            Adds a given number of days to a PlainDate.

                                            Equations
                                              Instances For
                                                @[inline]

                                                Subtracts a given number of days from a PlainDate.

                                                Equations
                                                  Instances For
                                                    @[inline]

                                                    Adds a given number of weeks to a PlainDate.

                                                    Equations
                                                      Instances For
                                                        @[inline]

                                                        Subtracts a given number of weeks from a PlainDate.

                                                        Equations
                                                          Instances For

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

                                                            Equations
                                                              Instances For
                                                                @[inline]

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

                                                                Equations
                                                                  Instances For

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

                                                                    Equations
                                                                      Instances For
                                                                        @[inline]

                                                                        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
                                                                          Instances For
                                                                            @[inline]

                                                                            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
                                                                              Instances For

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

                                                                                Equations
                                                                                  Instances For
                                                                                    @[inline]

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

                                                                                    Equations
                                                                                      Instances For
                                                                                        @[inline]

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

                                                                                        Equations
                                                                                          Instances For
                                                                                            @[inline]

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

                                                                                            Equations
                                                                                              Instances For
                                                                                                @[inline]

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

                                                                                                Equations
                                                                                                  Instances For
                                                                                                    @[inline]

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

                                                                                                    Equations
                                                                                                      Instances For
                                                                                                        @[inline]

                                                                                                        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
                                                                                                          Instances For
                                                                                                            @[inline]

                                                                                                            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
                                                                                                              Instances For
                                                                                                                @[inline]

                                                                                                                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
                                                                                                                  Instances For
                                                                                                                    @[inline]

                                                                                                                    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
                                                                                                                      Instances For

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

                                                                                                                        Equations
                                                                                                                          Instances For

                                                                                                                            Determines the week of the month for the given PlainDate. The week of the month is calculated based on the day of the month and the weekday. Each week starts on Monday because the entire library is based on the Gregorian Calendar.

                                                                                                                            Equations
                                                                                                                              Instances For

                                                                                                                                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
                                                                                                                                  Instances For

                                                                                                                                    Calculates the week of the year starting Monday for a given year.

                                                                                                                                    Equations
                                                                                                                                      Instances For