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.

instance Std.Time.instInhabitedValidDate {l : Bool} : Inhabited (ValidDate l)

instance Std.Time.instDecidableEqValidDate {leap : Bool} : DecidableEq (ValidDate leap)

instance Std.Time.instOrdValidDate {leap : Bool} : Ord (ValidDate leap)

instance Std.Time.instOrientedOrdValidDate {leap : Bool} : OrientedOrd (ValidDate leap)

instance Std.Time.instTransOrdValidDate {leap : Bool} : TransOrd (ValidDate leap)

instance Std.Time.instLawfulEqOrdValidDate {leap : Bool} : LawfulEqOrd (ValidDate leap)

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.

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.

@[irreducible]

def Std.Time.ValidDate.ofOrdinal.go {leap : Bool} (ordinal : Day.Ordinal.OfYear leap) (idx : Month.Ordinal) (acc : Int) (h : ordinal.val > acc) (p : acc = (Month.Ordinal.cumulativeDays leap idx).val) : ValidDate leap