Documentation

Time.Calendar.Days

structure Time.Day :

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

modifiedJulianDay : Int

Instances For

def Time.instBEqDay.beq :

Day → Day → Bool

Equations

Time.instBEqDay.beq { modifiedJulianDay := a } { modifiedJulianDay := b } = (a == b)
Time.instBEqDay.beq x✝¹ x✝ = false

Instances For

instance Time.instBEqDay :

Equations

Time.instBEqDay = { beq := Time.instBEqDay.beq }

instance Time.instToStringDay :

Equations

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

instance Time.instInhabitedDay :

modified julian day of january 1, year 1

Equations

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

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

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

Equations

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

Instances For

instance Time.Day.instLT :

Equations

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

instance Time.Day.instLE :

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