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

Equations

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

Instances For

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

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

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

- Std.Time.instDecidableEqValidDate = Subtype.instDecidableEq

source
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 }

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

Equations

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

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

Equations

- Std.Time.ValidDate.ofOrdinal ordinal = Std.Time.ValidDate.ofOrdinal.go✝ ordinal 1 0 ⋯ ⋯

Instances For