structure Time.LocalTime : Type

• localDay : Day
• localTimeOfDay : TimeOfDay

def Time.instBEqLocalTime.beq : LocalTime → LocalTime → Bool

Equations

• Time.instBEqLocalTime.beq { localDay := a, localTimeOfDay := a_1 } { localDay := b, localTimeOfDay := b_1 } = (a == b && a_1 == b_1)
• Time.instBEqLocalTime.beq x✝¹ x✝ = false

instance Time.instBEqLocalTime : BEq LocalTime

Equations

• Time.instBEqLocalTime = { beq := Time.instBEqLocalTime.beq }

def Lean.Parser.Category.datetime : Category

LocalTime syntactic category

Equations

• Lean.Parser.Category.datetime = { }

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

Equations

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

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

LocalTime from numeric literals year, month, day, hour, minute and second

Equations

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

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

Equations

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

instance Time.instToStringLocalTime : ToString LocalTime

Equations

• Time.instToStringLocalTime = { toString := fun (a : Time.LocalTime) => toString a.localDay ++ toString ", " ++ toString a.localTimeOfDay }

instance Time.instInhabitedLocalTime : Inhabited LocalTime

Equations

• Time.instInhabitedLocalTime = { default := { localDay := default, localTimeOfDay := default } }

def Time.LocalTime.addDays (n : Int) (lt : LocalTime) : LocalTime

Equations

• Time.LocalTime.addDays n lt = { localDay := Time.Day.addDays n lt.localDay, localTimeOfDay := lt.localTimeOfDay }

def Time.LocalTime.utcToLocalTime (tz : TimeZone) (utc : UTCTime) : LocalTime

Equations

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

def Time.LocalTime.localTimeToUTCTime (tz : TimeZone) (localTime : LocalTime) : UTCTime

Equations

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