Documentation

Std.Time.Date.ValidDate

source
def Std.Time.ValidDate (leap : Bool) :
Type

Represents a valid date for a given year, considering whether it is a leap year. Example: (2, 29) is valid only if leap is true.

Instances For
    source
    @[implicit_reducible]
    instance Std.Time.instInhabitedValidDate {l : Bool} :
    Inhabited (ValidDate l)
    source
    @[implicit_reducible]
    instance Std.Time.instDecidableEqValidDate {leap : Bool} :
    DecidableEq (ValidDate leap)
    source
    @[implicit_reducible]
    instance Std.Time.instOrdValidDate {leap : Bool} :
    Ord (ValidDate leap)
    source
    instance Std.Time.instOrientedOrdValidDate {leap : Bool} :
    OrientedOrd (ValidDate leap)
    source
    instance Std.Time.instTransOrdValidDate {leap : Bool} :
    TransOrd (ValidDate leap)
    source
    instance Std.Time.instLawfulEqOrdValidDate {leap : Bool} :
    LawfulEqOrd (ValidDate leap)
    source
    def Std.Time.ValidDate.dayOfYear {leap : Bool} (ordinal : ValidDate leap) :
    Day.Ordinal.OfYear leap

    Transforms a tuple of a Month and a Day into a Day.Ordinal.OfYear.

    Instances For
      source
      def Std.Time.ValidDate.ofOrdinal {leap : Bool} (ordinal : Day.Ordinal.OfYear leap) :
      ValidDate leap

      Transforms a Day.Ordinal.OfYear into a tuple of a Month and a Day.

      Instances For