structure Time.Day : Type

Modified Julian Day is a standard count of days, with zero being the day 1858-11-17

• modifiedJulianDay : Int

instance Time.instReprDay : Repr Day

Equations

• Time.instReprDay = { reprPrec := Time.reprDay✝ }

instance Time.instBEqDay : BEq Day

Equations

• Time.instBEqDay = { beq := Time.beqDay✝ }

instance Time.instToStringDay : ToString Day

Equations

• Time.instToStringDay = { toString := fun (a : Time.Day) => toString "mjd : " ++ toString a.modifiedJulianDay ++ toString "" }

instance Time.instInhabitedDay : Inhabited Day

modified julian day of january 1, year 1

Equations

• Time.instInhabitedDay = { default := { modifiedJulianDay := -678575 } }

def Time.Day.addDays (n : Int) (day : Day) : Day

Equations

• Time.Day.addDays n day = { modifiedJulianDay := day.modifiedJulianDay + n }

def Time.Day.diffDays (day1 day2 : Day) : Int

Equations

• day1.diffDays day2 = day1.modifiedJulianDay - day2.modifiedJulianDay

def Time.Day.lt (a b : Day) : Prop

Equations

• a.lt b = (a.modifiedJulianDay < b.modifiedJulianDay)

def Time.Day.le (a b : Day) : Prop

Equations

• a.le b = (a.modifiedJulianDay ≤ b.modifiedJulianDay)

instance Time.Day.instLT : LT Day

Equations

• Time.Day.instLT = { lt := Time.Day.lt }

instance Time.Day.instLE : LE Day

Equations

• Time.Day.instLE = { le := Time.Day.le }

instance Time.Day.instDecidableLt (a b : Day) : Decidable (a < b)

Equations

• a.instDecidableLt b = a.modifiedJulianDay.decLt b.modifiedJulianDay

instance Time.Day.instDecidableLe (a b : Day) : Decidable (a ≤ b)

Equations

• a.instDecidableLe b = a.modifiedJulianDay.decLe b.modifiedJulianDay