inductive Time.DayOfYear : Type

• common: Time.Icc 1 365 → Time.DayOfYear
• leap: Time.Icc 1 366 → Time.DayOfYear

instance Time.instReprDayOfYear : Repr Time.DayOfYear

Equations

• Time.instReprDayOfYear = { reprPrec := Time.reprDayOfYear✝ }

instance Time.instBEqDayOfYear : BEq Time.DayOfYear

Equations

• Time.instBEqDayOfYear = { beq := Time.beqDayOfYear✝ }

instance Time.instBEqDayOfYear_1 : BEq Time.DayOfYear

Equations

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

instance Time.instCoeDayOfYearIccOfNat : Coe Time.DayOfYear (Time.Icc 1 366)

Equations

• Time.instCoeDayOfYearIccOfNat = { coe := fun (x : Time.DayOfYear) => match x with | Time.DayOfYear.common d => ⟨d.val, ⋯⟩ | Time.DayOfYear.leap d => d }

def Time.isLeapYear (year : Int) : Bool

Is this year a leap year according to the proleptic Gregorian calendar?

Equations

• Time.isLeapYear year = (decide (year % 4 = 0) && (decide (year % 400 = 0) || !decide (year % 100 = 0)))

structure Time.OrdinalDate : Type

ISO 8601 Ordinal Date

• year : Int
• dayOfYear : Time.DayOfYear
• isValid : match self.dayOfYear with | Time.DayOfYear.common a => Time.isLeapYear self.year = false | Time.DayOfYear.leap a => Time.isLeapYear self.year = true

theorem Time.OrdinalDate.isValid (self : Time.OrdinalDate) : match self.dayOfYear with | Time.DayOfYear.common a => Time.isLeapYear self.year = false | Time.DayOfYear.leap a => Time.isLeapYear self.year = true

instance Time.instReprOrdinalDate : Repr Time.OrdinalDate

Equations

• Time.instReprOrdinalDate = { reprPrec := Time.reprOrdinalDate✝ }

instance Time.instBEqOrdinalDate : BEq Time.OrdinalDate

Equations

• Time.instBEqOrdinalDate = { beq := fun (a b : Time.OrdinalDate) => a.year == b.year && decide ((a.dayOfYear == b.dayOfYear) = true) }

def Time.dayOfYear (dayOfYear : Time.DayOfYear) : Nat

Equations

• Time.dayOfYear dayOfYear = match dayOfYear with | Time.DayOfYear.common d => d.val | Time.DayOfYear.leap d => d.val

theorem Time.year_emod_4_zero {qc : Int} {cent : Int} {q : Int} (year : Int) (h : year = qc * 400 + cent * 100 + q * 4 + 4) : year % 4 = 0

theorem Time.year_emod_400_zero {qc : Int} {cent : Int} {q : Int} (year : Int) (h1 : year = qc * 400 + cent * 100 + q * 4 + 4) (h2 : q = 24) (h3 : cent = 3) : year % 400 = 0

theorem Time.year_emod_100_non_zero {qc : Int} {cent : Int} {q : Int} (year : Int) (h1 : year = qc * 400 + cent * 100 + q * 4 + 4) (hle : 0 ≤ q) (h2 : q < 24) : year % 100 ≠ 0

theorem Time.isLeapYear_of_sum {qc : Int} {cent : Int} {q : Int} (year : Int) (h1 : year = qc * 400 + cent * 100 + q * 4 + 4) (hle : 0 ≤ q) (h2 : q ≤ 24) (h3 : q = 24 → cent = 3) : Time.isLeapYear year = true

def Time.toOrdinalDate (mjd : Time.Day) : Time.OrdinalDate

from modified Julian day to year and day of year

Equations

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

theorem Time.ite_ge {α : Type} (f : α → Bool) (v : α) (a : Nat) (b : Nat) (c : Nat) (h₁ : c ≤ a) (h₂ : c ≤ b) : c ≤ if f v = true then a else b

instance Time.instReprYearBase : Repr Time.YearBase

Equations

• Time.instReprYearBase = { reprPrec := Time.reprYearBase✝ }

instance Time.instBEqYearBase : BEq Time.YearBase

Equations

• Time.instBEqYearBase = { beq := Time.beqYearBase✝ }

def Time.firstDayOfYear (year : Int) : Time.DayOfYear

Equations

• Time.firstDayOfYear year = if Time.isLeapYear year = true then Time.DayOfYear.leap ⟨1, Time.firstDayOfYear.proof_1⟩ else Time.DayOfYear.common ⟨1, Time.firstDayOfYear.proof_2⟩

def Time.firstDayOfYearDate (year : Int) : Time.OrdinalDate

Equations

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

def Time.fromOrdinalDayOfYear (year : Int) (d : Time.Icc 1 366) : Time.Day

Convert from ISO 8601 Ordinal Date format. Invalid day numbers will be clipped to the correct range (1 to 365 or 366).

Equations

• Time.fromOrdinalDayOfYear year d = let day' := Time.clipDayOfYear Time.YearBase.One year ↑d.val; { modifiedJulianDay := Time.toModifiedJulianDay year day' }

def Time.fromOrdinalDate (dt : Time.OrdinalDate) : Time.Day

Convert from ISO 8601 Ordinal Date format. Invalid day numbers will be clipped to the correct range (1 to 365 or 366).

Equations

• Time.fromOrdinalDate dt = Time.fromOrdinalDayOfYear dt.year (match dt.dayOfYear with | Time.DayOfYear.common d => ⟨d.val, ⋯⟩ | Time.DayOfYear.leap d => d)

def Time.fromOrdinalDateValid (year : Int) (day : Int) : Option Time.Day

Convert from ISO 8601 Ordinal Date format.

Equations

• Time.fromOrdinalDateValid year day = do let day' ← Time.clipDayOfYearValid Time.YearBase.One year day pure { modifiedJulianDay := Time.toModifiedJulianDay year day' }

def Time.fromMondayStartWeekValid (year : Int) (w : Int) (d : Int) : Option Time.Day

The inverse of 'mondayStartWeek'. Get a 'Day' given the year, the number of the Monday-starting week, and the day of the week. The first Monday is the first day of week 1, any earlier days in the year are week 0 (as @%W@ in 'Data.Time.Format.formatTime').

Equations

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

def Time.fromSundayStartWeekValid (year : Int) (w : Int) (d : Int) : Option Time.Day

The inverse of 'sundayStartWeek'. Get a 'Day' given the year and the number of the day of a Sunday-starting week. The first Sunday is the first day of week 1, any earlier days in the year are week 0 (as @%U@ in 'Data.Time.Format.formatTime').

Equations

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