structure Time.TimeZone : Type

• timeZoneMinutes : Int
• timeZoneSummerOnly : Bool
• timeZoneName : String

instance Time.instReprTimeZone : Repr Time.TimeZone

Equations

• Time.instReprTimeZone = { reprPrec := Time.reprTimeZone✝ }

instance Time.instBEqTimeZone : BEq Time.TimeZone

Equations

• Time.instBEqTimeZone = { beq := Time.beqTimeZone✝ }

instance Time.instInhabitedTimeZone : Inhabited Time.TimeZone

Equations

• Time.instInhabitedTimeZone = { default := { timeZoneMinutes := 0, timeZoneSummerOnly := false, timeZoneName := "" } }

@[extern lean_get_current_timezone]

opaque Time.TimeZone.get_current_timezone : IO (Int × Int × String)

def Time.TimeZone.getTimeZone : IO Time.TimeZone

Equations

• Time.TimeZone.getTimeZone = do let tuple ← Time.TimeZone.get_current_timezone pure { timeZoneMinutes := tuple.fst / 60, timeZoneSummerOnly := tuple.snd.fst == 1, timeZoneName := tuple.snd.snd }

instance Time.TimeZone.instToString : ToString Time.TimeZone

Equations

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

def Time.TimeZone.minutesToTimeZone (m : Int) : Time.TimeZone

Equations

• Time.TimeZone.minutesToTimeZone m = { timeZoneMinutes := m, timeZoneSummerOnly := false, timeZoneName := "" }