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 Ordinal

Equations

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

instance Std.Time.Month.instOrdinalDecidableEq : DecidableEq Ordinal

Equations

• Std.Time.Month.instOrdinalDecidableEq = Std.Time.Internal.Bounded.instDecidableEq

instance Std.Time.Month.instOrdinalLE : LE Ordinal

Equations

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

instance Std.Time.Month.instOrdinalLT : LT Ordinal

Equations

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

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

Equations

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

instance Std.Time.Month.instInhabitedOrdinal : Inhabited Ordinal

Equations

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

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

Equations

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

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

Equations

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

instance Std.Time.Month.instOrdOrdinal : Ord Ordinal

Equations

• Std.Time.Month.instOrdOrdinal = inferInstanceAs (Ord (Std.Time.Internal.Bounded.LE 1 12))

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.

Equations

• Std.Time.Month.Offset = Int

instance Std.Time.Month.instOffsetRepr : Repr Offset

Equations

• Std.Time.Month.instOffsetRepr = instReprInt

instance Std.Time.Month.instOffsetDecidableEq : DecidableEq Offset

Equations

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

instance Std.Time.Month.instOffsetInhabited : Inhabited Offset

Equations

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

instance Std.Time.Month.instOffsetAdd : Add Offset

Equations

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

instance Std.Time.Month.instOffsetSub : Sub Offset

Equations

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

instance Std.Time.Month.instOffsetMul : Mul Offset

Equations

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

instance Std.Time.Month.instOffsetDiv : Div Offset

Equations

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

instance Std.Time.Month.instOffsetNeg : Neg Offset

Equations

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

instance Std.Time.Month.instOffsetToString : ToString Offset

Equations

• Std.Time.Month.instOffsetToString = instToStringInt

instance Std.Time.Month.instOffsetLT : LT Offset

Equations

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

instance Std.Time.Month.instOffsetLE : LE Offset

Equations

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

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

Equations

• Std.Time.Month.instDecidableLeOffset = Int.decLe x y

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

Equations

• Std.Time.Month.instDecidableLtOffset = Int.decLt x y

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

Equations

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

instance Std.Time.Month.instOrdOffset : Ord Offset

Equations

• Std.Time.Month.instOrdOffset = inferInstanceAs (Ord Int)

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.

Equations

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

instance Std.Time.Month.instQuarterRepr : Repr Quarter

Equations

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

instance Std.Time.Month.instQuarterDecidableEq : DecidableEq Quarter

Equations

• Std.Time.Month.instQuarterDecidableEq = Std.Time.Internal.Bounded.instDecidableEq

instance Std.Time.Month.instQuarterLT : LT Quarter

Equations

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

instance Std.Time.Month.instQuarterLE : LE Quarter

Equations

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

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

Equations

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

instance Std.Time.Month.instInhabitedQuarter : Inhabited Quarter

Equations

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

instance Std.Time.Month.instOrdQuarter : Ord Quarter

Equations

• Std.Time.Month.instOrdQuarter = inferInstanceAs (Ord (Std.Time.Internal.Bounded.LE 1 4))

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.

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) : 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) : Offset

Creates an Offset from an integer.

Equations

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

@[inline]

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

The ordinal value representing the month of January.

Equations

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

@[inline]

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

The ordinal value representing the month of February.

Equations

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

@[inline]

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

The ordinal value representing the month of March.

Equations

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

@[inline]

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

The ordinal value representing the month of April.

Equations

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

@[inline]

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

The ordinal value representing the month of May.

Equations

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

@[inline]

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

The ordinal value representing the month of June.

Equations

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

@[inline]

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

The ordinal value representing the month of July.

Equations

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

@[inline]

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

The ordinal value representing the month of August.

Equations

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

@[inline]

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

The ordinal value representing the month of September.

Equations

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

@[inline]

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

The ordinal value representing the month of October.

Equations

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

@[inline]

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

The ordinal value representing the month of November.

Equations

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

@[inline]

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

The ordinal value representing the month of December.

Equations

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

@[inline]

def Std.Time.Month.Ordinal.toOffset (month : Ordinal) : 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) : 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) : 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 : 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) : 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 : Ordinal) : 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 : Ordinal) : 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 : Ordinal) : 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 : Ordinal) : 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 : Ordinal) : 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 : 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.

Equations

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

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.

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 : Ordinal) (day : Day.Ordinal) : 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 : 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.