def Time.monthLengths (isleap : Bool) : List (Nat × Nat)

Equations

• Time.monthLengths isleap = [(1, 31), (2, if isleap = true then 29 else 28), (3, 31), (4, 30), (5, 31), (6, 30), (7, 31), (8, 31), (9, 30), (10, 31), (11, 30), (12, 31)]

def Time.monthLengths' (isleap : Bool) : Nat → Option Nat

Equations

• Time.monthLengths' isleap a = List.lookup a (Time.monthLengths isleap)

structure Time.Date : Type

Date in proleptic Gregorian calendar.

• Year : Int
• Month : Time.Icc 1 12
• Day : Time.Icc 1 31
• IsValid : ∃ (m : Nat × Nat), m ∈ Time.monthLengths (Time.isLeapYear self.Year) ∧ m.fst = self.Month.val ∧ self.Day.val ≤ m.snd

theorem Time.Date.IsValid (self : Time.Date) : ∃ (m : Nat × Nat), m ∈ Time.monthLengths (Time.isLeapYear self.Year) ∧ m.fst = self.Month.val ∧ self.Day.val ≤ m.snd

instance Time.instReprDate : Repr Time.Date

Equations

• Time.instReprDate = { reprPrec := Time.reprDate✝ }

def Time.Notation.date.quot : Lean.ParserDescr

Equations

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

def Lean.Parser.Category.date : Lean.Parser.Category

Date syntactic category

Equations

• Lean.Parser.Category.date = { }

def Time.Notation.«date__-___-__» : Lean.ParserDescr

Date from numeric literals year, month and day

Equations

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

def Time.Notation.«termDate%_» : Lean.ParserDescr

Equations

• Time.Notation.«termDate%_» = Lean.ParserDescr.node `Time.Notation.termDate%_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "date%") (Lean.ParserDescr.cat `date 0))

instance Time.instBEqDate : BEq Time.Date

Equations

• Time.instBEqDate = { beq := fun (a b : Time.Date) => decide (a.Year = b.Year) && decide (a.Month.val = b.Month.val) && decide (a.Day.val = b.Day.val) }

instance Time.instInhabitedDate : Inhabited Time.Date

Equations

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

def Time.monthLengths_sum (isleap : Bool) : Nat

Equations

• Time.monthLengths_sum isleap = List.foldl (fun (acc : Nat) (m : Nat × Nat) => acc + m.snd) 0 (Time.monthLengths isleap)

theorem Time.monthLengths_sum_eq (isleap : Bool) : (Time.monthLengths_sum isleap == if isleap = true then 366 else 365) = true

theorem Time.monthLengths_length_eq_12 (isleap : Bool) : ((Time.monthLengths isleap).length == 12) = true

theorem Time.monthLengths_length_gt_0 (isleap : Bool) : 0 < (Time.monthLengths isleap).length

theorem Time.monthLengths_month_in (isleap : Bool) (a : Nat × Nat) : a ∈ Time.monthLengths isleap → 1 ≤ a.fst ∧ a.fst ≤ 12

theorem Time.monthLengths_days_in (isleap : Bool) (a : Nat × Nat) : a ∈ Time.monthLengths isleap → 1 ≤ a.snd ∧ a.snd ≤ 31

theorem Time.list_foldl_init_add {α : Type u_1} (l : List α) (init : Nat) (v : Nat) (f : α → Nat) : List.foldl (fun (acc : Nat) (v : α) => f v + acc) init l + v = List.foldl (fun (acc : Nat) (v : α) => f v + acc) (init + v) l

def Time.ordinalDateToDate (dt : Time.OrdinalDate) : Time.Date

Equations

• Time.ordinalDateToDate dt = match h : dt.dayOfYear with | Time.DayOfYear.common yd => Time.findMonthDayCommon dt.year yd ⋯ | Time.DayOfYear.leap yd => Time.findMonthDayLeap dt.year yd ⋯

theorem Time.monthLengths_month_le_12 (isleap : Bool) (a : Nat × Nat) : a ∈ Time.monthLengths isleap → 1 ≤ a.fst ∧ a.fst ≤ 12

theorem Time.monthLengths_days_ge_28 (isleap : Bool) (a : Nat × Nat) : a ∈ Time.monthLengths isleap → 28 ≤ a.snd

theorem Time.monthLengths_days_le_31 (isleap : Bool) (a : Nat × Nat) : a ∈ Time.monthLengths isleap → a.snd ≤ 31

def Time.monthLength' (isLeap : Bool) (month' : Fin 12) : Nat

The length of a given month in the Gregorian or Julian calendars.

Equations

• Time.monthLength' isLeap month' = ((Time.monthLengths isLeap).get month').snd

theorem Time.monthLength'_ge_1 (isLeap : Bool) (month' : Fin 12) : 1 ≤ Time.monthLength' isLeap month'

theorem Time.monthLength'_le_31 (isLeap : Bool) (month' : Fin 12) : Time.monthLength' isLeap month' ≤ 31

theorem Time.monthAndDayToDayOfYear_gt_zero_of_month_gt (month : Int) (day : Int) (k : Int) (hm : 2 < month) (hk : -2 ≤ k) (hd : 0 < day) : 0 < (367 * month - 362) / 12 + k + day

theorem Time.monthAndDayToDayOfYear_le (month : Int) (day : Int) (k : Int) (hm : month ≤ 12) (hk : k = -2 ∨ k = -1) (hd2 : day ≤ 31) : (367 * month - 362) / 12 + k + day ≤ 366

theorem Time.days_le_31 (isLeap : Bool) (m : Fin 12) (day : Time.NonemptyIcc 1 (Time.monthLength' isLeap m)) : day.icc.val ≤ 31

def Time.monthAndDayToDayOfYear (isLeap : Bool) (month : Int) (day : Int) : Time.Icc 1 366

Convert month and day in the Gregorian or Julian calendars to day of year.

Equations

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

def Time.monthAndDayToDayOfYearValid (isLeap : Bool) (month : Int) (day : Int) : Option (Time.Icc 1 366)

Convert month and day in the Gregorian or Julian calendars to day of year option.

Equations

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