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.

Equations

• Std.Time.ValidDate leap = { val : Std.Time.Month.Ordinal × Std.Time.Day.Ordinal // Std.Time.Month.Ordinal.Valid leap val.fst val.snd }

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

def Std.Time.ValidDate.dayOfYear {leap : Bool} (ordinal : Std.Time.ValidDate leap) : Std.Time.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 : Std.Time.Day.Ordinal.OfYear leap) : Std.Time.ValidDate leap

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

Equations

• Std.Time.ValidDate.ofOrdinal ordinal = Std.Time.ValidDate.ofOrdinal.go ordinal 1 0 ⋯ ⋯

@[irreducible]

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

Equations

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