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 (ValidDate l)

Equations

• Std.Time.instInhabitedValidDate = { default := ⟨(1, 1), ⋯⟩ }

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

Equations

• Std.Time.instDecidableEqValidDate = Subtype.instDecidableEq

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

Equations

• Std.Time.instOrdValidDate = { compare := fun (a b : Std.Time.ValidDate leap) => compare a.val b.val }

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.

Equations

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

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.

Equations

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

@[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

Equations

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