def Time.Second.zero : Fixed Nano

Equations

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

def Time.Second.sixty : Fixed Nano

Equations

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

theorem Time.zero_lt_sixty : Second.zero < 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 : Ico 0 24
• Minute : Ico 0 60
• Second : Ico.Second

instance Time.instReprTimeOfDay : Repr TimeOfDay

Equations

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

instance Time.instBEqTimeOfDay : BEq TimeOfDay

Equations

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

instance Time.instToStringTimeOfDay : ToString TimeOfDay

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def Time.TimeOfDay.localToUTCTimeOfDay (zone : TimeZone) (tod : TimeOfDay) : Int × 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) (h3 : nanoSecs < 10 ^ 9) : Ico.Second

Equations

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

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

Equations

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

def Lean.Parser.Category.time : 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 TimeOfDay

Equations

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