structure Time.LocalTime : Type

• localDay : Time.Day
• localTimeOfDay : Time.TimeOfDay

instance Time.instReprLocalTime : Repr Time.LocalTime

Equations

• Time.instReprLocalTime = { reprPrec := Time.reprLocalTime✝ }

instance Time.instBEqLocalTime : BEq Time.LocalTime

Equations

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

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

Equations

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

def Lean.Parser.Category.datetime : Lean.Parser.Category

LocalTime syntactic category

Equations

• Lean.Parser.Category.datetime = { }

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 Time.LocalTime

Equations

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

instance Time.instInhabitedLocalTime : Inhabited Time.LocalTime

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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