def Std.Time.Month.Ordinal : Type

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

Equations

• Std.Time.Month.Ordinal = Std.Time.Internal.Bounded.LE 1 12

instance Std.Time.Month.instOrdinalRepr : Repr Std.Time.Month.Ordinal

Equations

• Std.Time.Month.instOrdinalRepr = Std.Time.Internal.Bounded.instRepr

instance Std.Time.Month.instOrdinalBEq : BEq Std.Time.Month.Ordinal

Equations

• Std.Time.Month.instOrdinalBEq = Std.Time.Internal.Bounded.instBEq

instance Std.Time.Month.instOrdinalLE : LE Std.Time.Month.Ordinal

Equations

• Std.Time.Month.instOrdinalLE = Std.Time.Internal.Bounded.instLE

instance Std.Time.Month.instOrdinalLT : LT Std.Time.Month.Ordinal

Equations

• Std.Time.Month.instOrdinalLT = Std.Time.Internal.Bounded.instLT

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

Equations

• Std.Time.Month.instOfNatOrdinal = inferInstanceAs (OfNat (Std.Time.Internal.Bounded.LE 1 (1 + ↑11)) n)

instance Std.Time.Month.instInhabitedOrdinal : Inhabited Std.Time.Month.Ordinal

Equations

• Std.Time.Month.instInhabitedOrdinal = { default := 1 }

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

Equations

• Std.Time.Month.instDecidableLeOrdinal = inferInstanceAs (Decidable (x.val ≤ y.val))

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

Equations

• Std.Time.Month.instDecidableLtOrdinal = inferInstanceAs (Decidable (x.val < y.val))

def Std.Time.Month.Offset : Type

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

Equations

• Std.Time.Month.Offset = Int

instance Std.Time.Month.instOffsetRepr : Repr Std.Time.Month.Offset

Equations

• Std.Time.Month.instOffsetRepr = instReprInt

instance Std.Time.Month.instOffsetBEq : BEq Std.Time.Month.Offset

Equations

• Std.Time.Month.instOffsetBEq = instBEqOfDecidableEq

instance Std.Time.Month.instOffsetInhabited : Inhabited Std.Time.Month.Offset

Equations

• Std.Time.Month.instOffsetInhabited = Int.instInhabited

instance Std.Time.Month.instOffsetAdd : Add Std.Time.Month.Offset

Equations

• Std.Time.Month.instOffsetAdd = Int.instAdd

instance Std.Time.Month.instOffsetSub : Sub Std.Time.Month.Offset

Equations

• Std.Time.Month.instOffsetSub = Int.instSub

instance Std.Time.Month.instOffsetMul : Mul Std.Time.Month.Offset

Equations

• Std.Time.Month.instOffsetMul = Int.instMul

instance Std.Time.Month.instOffsetDiv : Div Std.Time.Month.Offset

Equations

• Std.Time.Month.instOffsetDiv = Int.instDiv

instance Std.Time.Month.instOffsetNeg : Neg Std.Time.Month.Offset

Equations

• Std.Time.Month.instOffsetNeg = Int.instNegInt

instance Std.Time.Month.instOffsetToString : ToString Std.Time.Month.Offset

Equations

• Std.Time.Month.instOffsetToString = instToStringInt

instance Std.Time.Month.instOffsetLT : LT Std.Time.Month.Offset

Equations

• Std.Time.Month.instOffsetLT = Int.instLTInt

instance Std.Time.Month.instOffsetLE : LE Std.Time.Month.Offset

Equations

• Std.Time.Month.instOffsetLE = Int.instLEInt

instance Std.Time.Month.instOffsetDecidableEq : DecidableEq Std.Time.Month.Offset

Equations

• Std.Time.Month.instOffsetDecidableEq = Int.instDecidableEq

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

Equations

• Std.Time.Month.instOfNatOffset = { ofNat := Int.ofNat n }

def Std.Time.Month.Quarter : Type

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

Equations

• Std.Time.Month.Quarter = Std.Time.Internal.Bounded.LE 1 4

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

Determine the Quarter by the month.

Equations

• Std.Time.Month.Quarter.ofMonth month = ((Std.Time.Internal.Bounded.LE.sub month 1).ediv 3 Std.Time.Month.Quarter.ofMonth.proof_1).add 1

@[inline]

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

Creates an Offset from a natural number.

Equations

• Std.Time.Month.Offset.ofNat data = Int.ofNat data

@[inline]

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

Creates an Offset from an integer.

Equations

• Std.Time.Month.Offset.ofInt data = data

@[inline]

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

The ordinal value representing the month of January.

Equations

• Std.Time.Month.Ordinal.january = 1

@[inline]

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

The ordinal value representing the month of February.

Equations

• Std.Time.Month.Ordinal.february = 2

@[inline]

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

The ordinal value representing the month of March.

Equations

• Std.Time.Month.Ordinal.march = 3

@[inline]

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

The ordinal value representing the month of April.

Equations

• Std.Time.Month.Ordinal.april = 4

@[inline]

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

The ordinal value representing the month of May.

Equations

• Std.Time.Month.Ordinal.may = 5

@[inline]

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

The ordinal value representing the month of June.

Equations

• Std.Time.Month.Ordinal.june = 6

@[inline]

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

The ordinal value representing the month of July.

Equations

• Std.Time.Month.Ordinal.july = 7

@[inline]

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

The ordinal value representing the month of August.

Equations

• Std.Time.Month.Ordinal.august = 8

@[inline]

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

The ordinal value representing the month of September.

Equations

• Std.Time.Month.Ordinal.september = 9

@[inline]

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

The ordinal value representing the month of October.

Equations

• Std.Time.Month.Ordinal.october = 10

@[inline]

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

The ordinal value representing the month of November.

Equations

• Std.Time.Month.Ordinal.november = 11

@[inline]

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

The ordinal value representing the month of December.

Equations

• Std.Time.Month.Ordinal.december = 12

@[inline]

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

Converts a Ordinal into a Offset.

Equations

• month.toOffset = month.val

@[inline]

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

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

Equations

• Std.Time.Month.Ordinal.ofInt data h = Std.Time.Internal.Bounded.LE.mk data h

@[inline]

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

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

Equations

• Std.Time.Month.Ordinal.ofNat data h = Std.Time.Internal.Bounded.LE.ofNat' data h

@[inline]

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

Converts a Ordinal into a Nat.

Equations

• Std.Time.Month.Ordinal.toNat ⟨Int.ofNat s, property⟩ = s
• Std.Time.Month.Ordinal.toNat ⟨Int.negSucc s, h⟩ = nomatch ⋯

@[inline]

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

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

Equations

• Std.Time.Month.Ordinal.ofFin data = Std.Time.Internal.Bounded.LE.ofFin' data Std.Time.Month.Ordinal.ofFin.proof_1

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

Transforms Month.Ordinal into Second.Offset.

Equations

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

@[inline]

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

Transforms Month.Ordinal into Minute.Offset.

Equations

• Std.Time.Month.Ordinal.toMinutes leap month = Std.Time.Internal.UnitVal.ediv (Std.Time.Month.Ordinal.toSeconds leap month) 60

@[inline]

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

Transforms Month.Ordinal into Hour.Offset.

Equations

• Std.Time.Month.Ordinal.toHours leap month = Std.Time.Internal.UnitVal.ediv (Std.Time.Month.Ordinal.toMinutes leap month) 60

@[inline]

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

Transforms Month.Ordinal into Day.Offset.

Equations

• Std.Time.Month.Ordinal.toDays leap month = Std.Time.Internal.UnitVal.convert (Std.Time.Month.Ordinal.toSeconds leap month)

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

Gets the number of days in a month.

Equations

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

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

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

Returns the number of days until the month.

Equations

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

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

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

@[reducible, inline]

abbrev Std.Time.Month.Ordinal.Valid (leap : Bool) (month : Std.Time.Month.Ordinal) (day : Std.Time.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.

Equations

• Std.Time.Month.Ordinal.Valid leap month day = (day.val ≤ (Std.Time.Month.Ordinal.days leap month).val)

@[inline]

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

Clips the day to be within the valid range.

Equations

• Std.Time.Month.Ordinal.clipDay leap month day = if day.val > (Std.Time.Month.Ordinal.days leap month).val then Std.Time.Month.Ordinal.days leap month else day

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

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