def Std.Time.Month.Ordinal : Type

Ordinal represents a bounded value for months, which ranges between 1 and 12.

@[implicit_reducible]

instance Std.Time.Month.instReprOrdinal : Repr Ordinal

@[implicit_reducible]

instance Std.Time.Month.instDecidableEqOrdinal : DecidableEq Ordinal

@[implicit_reducible]

instance Std.Time.Month.instLEOrdinal : LE Ordinal

@[implicit_reducible]

instance Std.Time.Month.instLTOrdinal : LT Ordinal

@[implicit_reducible]

instance Std.Time.Month.instOfNatOrdinal {n : Nat} : OfNat Ordinal n

@[implicit_reducible]

instance Std.Time.Month.instInhabitedOrdinal : Inhabited Ordinal

@[implicit_reducible]

instance Std.Time.Month.instDecidableLeOrdinal {x y : Ordinal} : Decidable (x ≤ y)

@[implicit_reducible]

instance Std.Time.Month.instDecidableLtOrdinal {x y : Ordinal} : Decidable (x < y)

@[implicit_reducible]

instance Std.Time.Month.instOrdOrdinal : Ord Ordinal

instance Std.Time.Month.instTransOrdOrdinal : TransOrd Ordinal

instance Std.Time.Month.instLawfulEqOrdOrdinal : LawfulEqOrd Ordinal

def Std.Time.Month.Offset : Type

Offset represents an offset in months. It is defined as an Int.

@[implicit_reducible]

instance Std.Time.Month.instReprOffset : Repr Offset

@[implicit_reducible]

instance Std.Time.Month.instDecidableEqOffset : DecidableEq Offset

@[implicit_reducible]

instance Std.Time.Month.instInhabitedOffset : Inhabited Offset

@[implicit_reducible]

instance Std.Time.Month.instAddOffset : Add Offset

@[implicit_reducible]

instance Std.Time.Month.instSubOffset : Sub Offset

@[implicit_reducible]

instance Std.Time.Month.instMulOffset : Mul Offset

@[implicit_reducible]

instance Std.Time.Month.instDivOffset : Div Offset

@[implicit_reducible]

instance Std.Time.Month.instNegOffset : Neg Offset

@[implicit_reducible]

instance Std.Time.Month.instToStringOffset : ToString Offset

@[implicit_reducible]

instance Std.Time.Month.instLTOffset : LT Offset

@[implicit_reducible]

instance Std.Time.Month.instLEOffset : LE Offset

@[implicit_reducible]

instance Std.Time.Month.instDecidableLeOffset {x y : Offset} : Decidable (x ≤ y)

@[implicit_reducible]

instance Std.Time.Month.instDecidableLtOffset {x y : Offset} : Decidable (x < y)

@[implicit_reducible]

instance Std.Time.Month.instOfNatOffset {n : Nat} : OfNat Offset n

@[implicit_reducible]

instance Std.Time.Month.instOrdOffset : Ord Offset

instance Std.Time.Month.instTransOrdOffset : TransOrd Offset

instance Std.Time.Month.instLawfulEqOrdOffset : LawfulEqOrd Offset

def Std.Time.Month.Quarter : Type

Quarter represents a value between 1 and 4, inclusive, corresponding to the four quarters of a year.

@[implicit_reducible]

instance Std.Time.Month.instReprQuarter : Repr Quarter

@[implicit_reducible]

instance Std.Time.Month.instDecidableEqQuarter : DecidableEq Quarter

@[implicit_reducible]

instance Std.Time.Month.instLTQuarter : LT Quarter

@[implicit_reducible]

instance Std.Time.Month.instLEQuarter : LE Quarter

@[implicit_reducible]

instance Std.Time.Month.instOfNatQuarter {n : Nat} : OfNat Quarter n

@[implicit_reducible]

instance Std.Time.Month.instInhabitedQuarter : Inhabited Quarter

@[implicit_reducible]

instance Std.Time.Month.instOrdQuarter : Ord Quarter

instance Std.Time.Month.instTransOrdQuarter : TransOrd Quarter

instance Std.Time.Month.instLawfulEqOrdQuarter : LawfulEqOrd Quarter

def Std.Time.Month.Quarter.ofMonth (month : Ordinal) : Quarter

Determine the Quarter by the month.

@[inline]

def Std.Time.Month.Offset.ofNat (data : Nat) : Offset

Creates an Offset from a natural number.

@[inline]

def Std.Time.Month.Offset.ofInt (data : Int) : Offset

Creates an Offset from an integer.

@[inline]

def Std.Time.Month.Ordinal.january : Ordinal

The ordinal value representing the month of January.

@[inline]

def Std.Time.Month.Ordinal.february : Ordinal

The ordinal value representing the month of February.

@[inline]

def Std.Time.Month.Ordinal.march : Ordinal

The ordinal value representing the month of March.

@[inline]

def Std.Time.Month.Ordinal.april : Ordinal

The ordinal value representing the month of April.

@[inline]

def Std.Time.Month.Ordinal.may : Ordinal

The ordinal value representing the month of May.

@[inline]

def Std.Time.Month.Ordinal.june : Ordinal

The ordinal value representing the month of June.

@[inline]

def Std.Time.Month.Ordinal.july : Ordinal

The ordinal value representing the month of July.

@[inline]

def Std.Time.Month.Ordinal.august : Ordinal

The ordinal value representing the month of August.

@[inline]

def Std.Time.Month.Ordinal.september : Ordinal

The ordinal value representing the month of September.

@[inline]

def Std.Time.Month.Ordinal.october : Ordinal

The ordinal value representing the month of October.

@[inline]

def Std.Time.Month.Ordinal.november : Ordinal

The ordinal value representing the month of November.

@[inline]

def Std.Time.Month.Ordinal.december : Ordinal

The ordinal value representing the month of December.

@[inline]

def Std.Time.Month.Ordinal.toOffset (month : Ordinal) : Offset

Converts a Ordinal into a Offset.

@[inline]

def Std.Time.Month.Ordinal.ofInt (data : Int) (h : 1 ≤ data ∧ data ≤ 12) : Ordinal

Creates an Ordinal from an integer, ensuring the value is within bounds.

@[inline]

def Std.Time.Month.Ordinal.ofNat (data : Nat) (h : data ≥ 1 ∧ data ≤ 12 := by decide) : Ordinal

Creates an Ordinal from a Nat, ensuring the value is within bounds.

@[inline]

def Std.Time.Month.Ordinal.toNat (month : Ordinal) : Nat

Converts a Ordinal into a Nat.

@[inline]

def Std.Time.Month.Ordinal.ofFin (data : Fin 13) : Ordinal

Creates an Ordinal from a Fin, ensuring the value is within bounds, if its 0 then its converted to 1.

def Std.Time.Month.Ordinal.toSeconds (leap : Bool) (month : Ordinal) : Second.Offset

Transforms Month.Ordinal into Second.Offset.

@[inline]

def Std.Time.Month.Ordinal.toMinutes (leap : Bool) (month : Ordinal) : Minute.Offset

Transforms Month.Ordinal into Minute.Offset.

@[inline]

def Std.Time.Month.Ordinal.toHours (leap : Bool) (month : Ordinal) : Hour.Offset

Transforms Month.Ordinal into Hour.Offset.

@[inline]

def Std.Time.Month.Ordinal.toDays (leap : Bool) (month : Ordinal) : Day.Offset

Transforms Month.Ordinal into Day.Offset.

def Std.Time.Month.Ordinal.days (leap : Bool) (month : Ordinal) : Day.Ordinal

Gets the number of days in a month.

theorem Std.Time.Month.Ordinal.days_gt_27 (leap : Bool) (i : Ordinal) : days leap i > 27

def Std.Time.Month.Ordinal.cumulativeDays (leap : Bool) (month : Ordinal) : Day.Offset

Returns the number of days until the month.

theorem Std.Time.Month.Ordinal.cumulativeDays_le (leap : Bool) (month : Ordinal) : cumulativeDays leap month ≥ 0 ∧ cumulativeDays leap month ≤ 334 + if leap = true then 1 else 0

theorem Std.Time.Month.Ordinal.difference_eq {leap : Bool} {month : Ordinal} (p : month.val ≤ 11) : have next := (Internal.Bounded.LE.truncateTop month p).addTop 1 difference_eq._proof_1; (cumulativeDays leap next).val = (cumulativeDays leap month).val + (days leap month).val

@[reducible, inline]

abbrev Std.Time.Month.Ordinal.Valid (leap : Bool) (month : Ordinal) (day : Day.Ordinal) : Prop

Checks if a given day is valid for the specified month and year. For example, 29/02 is valid only if the year is a leap year.

@[inline]

def Std.Time.Month.Ordinal.clipDay (leap : Bool) (month : Ordinal) (day : Day.Ordinal) : Day.Ordinal

Clips the day to be within the valid range.

theorem Std.Time.Month.Ordinal.valid_clipDay {leap : Bool} {month : Ordinal} {day : Day.Ordinal} : Valid leap month (clipDay leap month day)

Proves that every value provided by a clipDay is a valid day in a year.