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.instCoeIccOfNat : Coe (Time.Icc 1 365) (Time.Icc 1 366)

Equations

• Time.instCoeIccOfNat = { coe := fun (d : Time.Icc 1 365) => ⟨d.val, ⋯⟩ }

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.ext {x y : Time.OrdinalDate} (year : x.year = y.year) (dayOfYear : x.dayOfYear = y.dayOfYear) : x = y

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) }

instance Time.instToStringOrdinalDate : ToString Time.OrdinalDate

Equations

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

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

Equations

• Time.dayOfYear (Time.DayOfYear.common a) = a.val
• Time.dayOfYear (Time.DayOfYear.leap a) = a.val

def Time.toDayOfYear (year d' : Int) : Time.OrdinalDate

Equations

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

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

theorem Time.year_emod_400_zero {qc cent 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 cent 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 cent q 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.

def Time.toModifiedJulianDay (year : Int) (dayOfYear : Nat) : Int

Equations

• Time.toModifiedJulianDay year dayOfYear = ↑dayOfYear + 365 * (year - 1) + (year - 1) / 4 - (year - 1) / 100 + (year - 1) / 400 + (default.modifiedJulianDay - 1)

theorem Time.ite_ge {α : Type} (f : α → Bool) (v : α) (a b 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.clipDayOfYear (b : Time.YearBase) (year dayOfYear : Int) : Nat

Equations

• Time.clipDayOfYear Time.YearBase.Zero year dayOfYear = Time.Clip.clip 0 (if Time.isLeapYear year = true then 365 else 364) dayOfYear ⋯
• Time.clipDayOfYear Time.YearBase.One year dayOfYear = Time.Clip.clip 1 (if Time.isLeapYear year = true then 366 else 365) dayOfYear ⋯

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 = { modifiedJulianDay := Time.toModifiedJulianDay year (Time.clipDayOfYear Time.YearBase.One year ↑d.val) }

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

Convert from ISO 8601 Ordinal Date format.

Equations

• Time.fromOrdinalDate dt = { modifiedJulianDay := Time.toModifiedJulianDay dt.year (Time.dayOfYear dt.dayOfYear) }

def Time.fromOrdinalDateValid (year 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 w 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 w 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.

def Time.OrdinalDate.addDays (n : Int) (dt : Time.OrdinalDate) : Time.OrdinalDate

Equations

• Time.OrdinalDate.addDays n dt = Time.toOrdinalDate (Time.Day.addDays n (Time.fromOrdinalDate dt))