structure Time.TimeZone : Type

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

def Time.instBEqTimeZone.beq : TimeZone → TimeZone → Bool

Equations

• One or more equations did not get rendered due to their size.
• Time.instBEqTimeZone.beq x✝¹ x✝ = false

instance Time.instBEqTimeZone : BEq TimeZone

Equations

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

instance Time.instInhabitedTimeZone : Inhabited 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 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 TimeZone

Equations

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

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

Equations

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