def Time.Second.zero : Time.Fixed Time.Nano

Equations

• Time.Second.zero = Time.Fixed.zero

def Time.Second.sixty : Time.Fixed Time.Nano

Equations

• Time.Second.sixty = Time.Fixed.toFixed Time.Sign.Nonneg 60 default

theorem Time.zero_lt_sixty : Time.Second.zero < Time.Second.sixty

@[reducible, inline]

abbrev Time.Ico.Second : Type

Equations

• Time.Ico.Second = Time.Ico Time.Second.zero Time.Second.sixty

structure Time.TimeOfDay : Type

• Hour : Time.Ico 0 24
• Minute : Time.Ico 0 60
• Second : Time.Ico.Second

instance Time.instReprTimeOfDay : Repr Time.TimeOfDay

Equations

• Time.instReprTimeOfDay = { reprPrec := Time.reprTimeOfDay✝ }

instance Time.instBEqTimeOfDay : BEq Time.TimeOfDay

Equations

• Time.instBEqTimeOfDay = { beq := Time.beqTimeOfDay✝ }

instance Time.instToStringTimeOfDay : ToString Time.TimeOfDay

Equations

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

def Time.TimeOfDay.timeOfDayToTime (tod : Time.TimeOfDay) : Time.DiffTime

Equations

• tod.timeOfDayToTime = let p := tod.Second.val.toParts; Time.DiffTime.fromSecNsec Time.Sign.Nonneg ((tod.Hour.val * 60 + tod.Minute.val) * 60 + p.numerator) p.denominator

def Time.TimeOfDay.timeToDaysAndTimeOfDay (secsOfTime : Time.DiffTime) : Int × Time.TimeOfDay

Equations

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

def Time.TimeOfDay.timeToTimeOfDay (secsOfTime : Time.DiffTime) : Time.TimeOfDay

Equations

• Time.TimeOfDay.timeToTimeOfDay secsOfTime = (Time.TimeOfDay.timeToDaysAndTimeOfDay secsOfTime).snd

def Time.TimeOfDay.utcToLocalTimeOfDay (zone : Time.TimeZone) (tod : Time.TimeOfDay) : Int × Time.TimeOfDay

Equations

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

def Time.TimeOfDay.localToUTCTimeOfDay (zone : Time.TimeZone) (tod : Time.TimeOfDay) : Int × Time.TimeOfDay

Equations

• Time.TimeOfDay.localToUTCTimeOfDay zone tod = Time.TimeOfDay.utcToLocalTimeOfDay (Time.TimeZone.minutesToTimeZone (-zone.timeZoneMinutes)) tod

def Time.TimeOfDay.toSecond (secs : Int) (nanoSecs : Nat) (h1 : 0 ≤ secs) (h2 : secs < 60) : Time.Ico.Second

Equations

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

def Time.TimeOfDay.toSecond' (s : Time.NonemptyIco 0 60) : Time.Ico.Second

Equations

• Time.TimeOfDay.toSecond' s = Time.TimeOfDay.toSecond (↑s.ico.val) 0 ⋯ ⋯

def Lean.Parser.Category.time : Lean.Parser.Category

TimeOfDay syntactic category

Equations

• Lean.Parser.Category.time = { }

def Time.TimeOfDay.Time.Notation.time.quot : Lean.ParserDescr

Equations

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

def Time.TimeOfDay.Time.Notation.«time__:___:__» : Lean.ParserDescr

TimeOfDay from numeric literals hour, minute, second and nanosecond

Equations

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

def Time.TimeOfDay.Time.Notation.«time__:___:___1» : Lean.ParserDescr

TimeOfDay from numeric literals hour, minute and second

Equations

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

def Time.TimeOfDay.Time.Notation.«termTime%_» : Lean.ParserDescr

Equations

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

instance Time.TimeOfDay.instInhabited : Inhabited Time.TimeOfDay

Equations

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