def Std.Time.Month.Ordinal : Type

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

instance Std.Time.Month.instOrdinalRepr : Repr Ordinal

instance Std.Time.Month.instOrdinalDecidableEq : DecidableEq Ordinal

instance Std.Time.Month.instOrdinalLE : LE Ordinal

instance Std.Time.Month.instOrdinalLT : LT Ordinal

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

instance Std.Time.Month.instInhabitedOrdinal : Inhabited Ordinal

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

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

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.

instance Std.Time.Month.instOffsetRepr : Repr Offset

instance Std.Time.Month.instOffsetDecidableEq : DecidableEq Offset

instance Std.Time.Month.instOffsetInhabited : Inhabited Offset

instance Std.Time.Month.instOffsetAdd : Add Offset

instance Std.Time.Month.instOffsetSub : Sub Offset

instance Std.Time.Month.instOffsetMul : Mul Offset

instance Std.Time.Month.instOffsetDiv : Div Offset

instance Std.Time.Month.instOffsetNeg : Neg Offset

instance Std.Time.Month.instOffsetToString : ToString Offset

instance Std.Time.Month.instOffsetLT : LT Offset

instance Std.Time.Month.instOffsetLE : LE Offset

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

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

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

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.

instance Std.Time.Month.instQuarterRepr : Repr Quarter

instance Std.Time.Month.instQuarterDecidableEq : DecidableEq Quarter

instance Std.Time.Month.instQuarterLT : LT Quarter

instance Std.Time.Month.instQuarterLE : LE Quarter

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

instance Std.Time.Month.instInhabitedQuarter : Inhabited Quarter

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) : let next := (Internal.Bounded.LE.truncateTop month p).addTop 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.