diff --git a/src/Std/Time/DateTime.lean b/src/Std/Time/DateTime.lean
index ec83e83f0790..8f223bd0a1ef 100644
--- a/src/Std/Time/DateTime.lean
+++ b/src/Std/Time/DateTime.lean
@@ -50,7 +50,7 @@ def toPlainDateAssumingUTC (timestamp : Timestamp) : PlainDate :=
 Converts a `Timestamp` to a `PlainTime`
 -/
 @[inline]
-def getTimeAssumingUTC (timestamp : Timestamp) : PlainTime :=
+def getTimeAssumingUTC (timestamp : Timestamp) : PlainTime leap :=
   let nanos := timestamp.toNanosecondsSinceUnixEpoch
   PlainTime.ofNanoseconds nanos
 
@@ -75,7 +75,7 @@ Converts a `PlainDate` to a `Timestamp`
 -/
 @[inline]
 def ofPlainDate (date : PlainDate) : PlainDateTime :=
-  { date, time := PlainTime.midnight }
+  { date, time := Sigma.mk true (PlainTime.midnight) }
 
 /--
 Converts a `PlainDateTime` to a `PlainDate`
@@ -88,15 +88,15 @@ def toPlainDate (pdt : PlainDateTime) : PlainDate :=
 Converts a `PlainTime` to a `PlainDateTime`
 -/
 @[inline]
-def ofPlainTime (time : PlainTime) : PlainDateTime :=
-  { date := ⟨1, 1, 1, by decide⟩, time }
+def ofPlainTime (time : PlainTime leap) : PlainDateTime :=
+  { date := ⟨1, 1, 1, by decide⟩, time := Sigma.mk leap time }
 
 /--
 Converts a `PlainDateTime` to a `PlainTime`
 -/
 @[inline]
-def toPlainTime (pdt : PlainDateTime) : PlainTime :=
-  pdt.time
+def toPlainTime (pdt : PlainDateTime) : PlainTime pdt.time.fst :=
+  pdt.time.snd
 
 instance : HSub PlainDateTime PlainDateTime Duration where
   hSub x y := x.toTimestampAssumingUTC - y.toTimestampAssumingUTC
diff --git a/src/Std/Time/DateTime/PlainDateTime.lean b/src/Std/Time/DateTime/PlainDateTime.lean
index 7949c9930b5b..ddc5a2643a27 100644
--- a/src/Std/Time/DateTime/PlainDateTime.lean
+++ b/src/Std/Time/DateTime/PlainDateTime.lean
@@ -28,9 +28,16 @@ structure PlainDateTime where
   /--
   The `Time` component of a `PlainTime`
   -/
-  time : PlainTime
+  time : Sigma PlainTime
+
+  deriving Repr
+
+instance : Inhabited PlainDateTime where
+  default := {
+    date := Inhabited.default,
+    time := Sigma.mk true Inhabited.default
+  }
 
-  deriving Inhabited, BEq, Repr
 
 namespace PlainDateTime
 
@@ -39,8 +46,8 @@ Converts a `PlainDateTime` to a `Timestamp`
 -/
 def toTimestampAssumingUTC (dt : PlainDateTime) : Timestamp :=
   let days := dt.date.toDaysSinceUNIXEpoch
-  let nanos := days.toSeconds + dt.time.toSeconds |>.mul 1000000000
-  let nanos := nanos.val + dt.time.nanosecond.val
+  let nanos := days.toSeconds + dt.time.snd.toSeconds |>.mul 1000000000
+  let nanos := nanos.val + dt.time.snd.nanosecond.val
   Timestamp.ofNanosecondsSinceUnixEpoch (Nanosecond.Offset.ofInt nanos)
 
 /--
@@ -123,7 +130,7 @@ def ofTimestampAssumingUTC (stamp : Timestamp) : PlainDateTime := Id.run do
 
   return {
     date := PlainDate.ofYearMonthDayClip year hmon (Day.Ordinal.ofFin (Fin.succ mday))
-    time := PlainTime.ofHourMinuteSecondsNano (leap := false) (hour.expandTop (by decide)) minute second nano
+    time := Sigma.mk false (PlainTime.ofHourMinuteSecondsNano (hour.expandTop (by decide)) minute second nano)
   }
 
 /--
@@ -137,8 +144,8 @@ def toDaysSinceUNIXEpoch (pdt : PlainDateTime) : Day.Offset :=
 Converts a `PlainDateTime` to the number of days since the UNIX epoch.
 -/
 @[inline]
-def ofDaysSinceUNIXEpoch (days : Day.Offset) (time : PlainTime) : PlainDateTime :=
-  PlainDateTime.mk (PlainDate.ofDaysSinceUNIXEpoch days) time
+def ofDaysSinceUNIXEpoch (days : Day.Offset) (time : PlainTime leap) : PlainDateTime :=
+  PlainDateTime.mk (PlainDate.ofDaysSinceUNIXEpoch days) (Sigma.mk leap time)
 
 /--
 Sets the `PlainDateTime` to the specified `desiredWeekday`.
@@ -199,35 +206,35 @@ Creates a new `PlainDateTime` by adjusting the `hour` component of its `time` to
 -/
 @[inline]
 def withHours (dt : PlainDateTime) (hour : Hour.Ordinal) : PlainDateTime :=
-  { dt with time := { dt.time with hour := hour } }
+  { dt with time := Sigma.mk dt.time.fst { dt.time.snd with hour := hour } }
 
 /--
 Creates a new `PlainDateTime` by adjusting the `minute` component of its `time` to the given value.
 -/
 @[inline]
 def withMinutes (dt : PlainDateTime) (minute : Minute.Ordinal) : PlainDateTime :=
-  { dt with time := { dt.time with minute := minute } }
+  { dt with time := Sigma.mk dt.time.fst { dt.time.snd with minute := minute } }
 
 /--
 Creates a new `PlainDateTime` by adjusting the `second` component of its `time` to the given value.
 -/
 @[inline]
-def withSeconds (dt : PlainDateTime) (second : Sigma Second.Ordinal) : PlainDateTime :=
-  { dt with time := { dt.time with second := second } }
+def withSeconds (dt : PlainDateTime) (second : Second.Ordinal α) : PlainDateTime :=
+  { dt with time := Sigma.mk α { dt.time.snd with second := second } }
 
 /--
 Creates a new `PlainDateTime` by adjusting the milliseconds component inside the `nano` component of its `time` to the given value.
 -/
 @[inline]
 def withMilliseconds (dt : PlainDateTime) (millis : Millisecond.Ordinal) : PlainDateTime :=
-  { dt with time := dt.time.withMilliseconds millis }
+  { dt with time := Sigma.mk dt.time.fst (dt.time.snd.withMilliseconds millis) }
 
 /--
 Creates a new `PlainDateTime` by adjusting the `nano` component of its `time` to the given value.
 -/
 @[inline]
 def withNanoseconds (dt : PlainDateTime) (nano : Nanosecond.Ordinal) : PlainDateTime :=
-  { dt with time := dt.time.withNanoseconds nano }
+  { dt with time := Sigma.mk dt.time.fst (dt.time.snd.withNanoseconds nano) }
 
 /--
 Adds a `Day.Offset` to a `PlainDateTime`.
@@ -322,10 +329,10 @@ Adds an `Hour.Offset` to a `PlainDateTime`, adjusting the date if the hour overf
 -/
 @[inline]
 def addHours (dt : PlainDateTime) (hours : Hour.Offset) : PlainDateTime :=
-  let totalSeconds := dt.time.toSeconds + hours.toSeconds
+  let totalSeconds := dt.time.snd.toSeconds + hours.toSeconds
   let days := totalSeconds.ediv 86400
-  let newTime := dt.time.addSeconds (hours.toSeconds)
-  { dt with date := dt.date.addDays days, time := newTime }
+  let newTime := dt.time.snd.addSeconds (hours.toSeconds)
+  { dt with date := dt.date.addDays days, time := Sigma.mk dt.time.fst newTime }
 
 /--
 Subtracts an `Hour.Offset` from a `PlainDateTime`, adjusting the date if the hour underflows.
@@ -339,10 +346,10 @@ Adds a `Minute.Offset` to a `PlainDateTime`, adjusting the hour and date if the
 -/
 @[inline]
 def addMinutes (dt : PlainDateTime) (minutes : Minute.Offset) : PlainDateTime :=
-  let totalSeconds := dt.time.toSeconds + minutes.toSeconds
+  let totalSeconds := dt.time.snd.toSeconds + minutes.toSeconds
   let days := totalSeconds.ediv 86400
-  let newTime := dt.time.addSeconds (minutes.toSeconds)
-  { dt with date := dt.date.addDays days, time := newTime }
+  let newTime := dt.time.snd.addSeconds (minutes.toSeconds)
+  { dt with date := dt.date.addDays days, time := Sigma.mk dt.time.fst newTime }
 
 /--
 Subtracts a `Minute.Offset` from a `PlainDateTime`, adjusting the hour and date if the minutes underflow.
@@ -356,10 +363,10 @@ Adds a `Second.Offset` to a `PlainDateTime`, adjusting the minute, hour, and dat
 -/
 @[inline]
 def addSeconds (dt : PlainDateTime) (seconds : Second.Offset) : PlainDateTime :=
-  let totalSeconds := dt.time.toSeconds + seconds
+  let totalSeconds := dt.time.snd.toSeconds + seconds
   let days := totalSeconds.ediv 86400
-  let newTime := dt.time.addSeconds seconds
-  { dt with date := dt.date.addDays days, time := newTime }
+  let newTime := dt.time.snd.addSeconds seconds
+  { dt with date := dt.date.addDays days, time := Sigma.mk dt.time.fst newTime }
 
 /--
 Subtracts a `Second.Offset` from a `PlainDateTime`, adjusting the minute, hour, and date if the seconds underflow.
@@ -373,10 +380,10 @@ Adds a `Millisecond.Offset` to a `PlainDateTime`, adjusting the second, minute,
 -/
 @[inline]
 def addMilliseconds (dt : PlainDateTime) (milliseconds : Millisecond.Offset) : PlainDateTime :=
-  let totalMilliseconds := dt.time.toMilliseconds + milliseconds
+  let totalMilliseconds := dt.time.snd.toMilliseconds + milliseconds
   let days := totalMilliseconds.ediv 86400000 -- 86400000 ms in a day
-  let newTime := dt.time.addMilliseconds milliseconds
-  { dt with date := dt.date.addDays days, time := newTime }
+  let newTime := dt.time.snd.addMilliseconds milliseconds
+  { dt with date := dt.date.addDays days, time := Sigma.mk dt.time.fst newTime }
 
 /--
 Subtracts a `Millisecond.Offset` from a `PlainDateTime`, adjusting the second, minute, hour, and date if the milliseconds underflow.
@@ -390,12 +397,12 @@ Adds a `Nanosecond.Offset` to a `PlainDateTime`, adjusting the seconds, minutes,
 -/
 @[inline]
 def addNanoseconds (dt : PlainDateTime) (nanos : Nanosecond.Offset) : PlainDateTime :=
-  let nano := Nanosecond.Offset.ofInt dt.time.nanosecond.val
+  let nano := Nanosecond.Offset.ofInt dt.time.snd.nanosecond.val
   let totalNanos := nano + nanos
   let extraSeconds := totalNanos.ediv 1000000000
   let nanosecond := Bounded.LE.byEmod totalNanos.val 1000000000 (by decide)
-  let newTime := dt.time.addSeconds extraSeconds
-  { dt with time := { newTime with nanosecond } }
+  let newTime := dt.time.snd.addSeconds extraSeconds
+  { dt with time := Sigma.mk dt.time.fst { newTime with nanosecond } }
 
 /--
 Subtracts a `Nanosecond.Offset` from a `PlainDateTime`, adjusting the seconds, minutes, hours, and date if the nanoseconds underflow.
@@ -437,35 +444,35 @@ Getter for the `Hour` inside of a `PlainDateTime`.
 -/
 @[inline]
 def hour (dt : PlainDateTime) : Hour.Ordinal :=
-  dt.time.hour
+  dt.time.snd.hour
 
 /--
 Getter for the `Minute` inside of a `PlainDateTime`.
 -/
 @[inline]
 def minute (dt : PlainDateTime) : Minute.Ordinal :=
-  dt.time.minute
+  dt.time.snd.minute
 
 /--
 Getter for the `Millisecond` inside of a `PlainDateTime`.
 -/
 @[inline]
 def millisecond (dt : PlainDateTime) : Millisecond.Ordinal :=
-  dt.time.millisecond
+  dt.time.snd.millisecond
 
 /--
 Getter for the `Second` inside of a `PlainDateTime`.
 -/
 @[inline]
-def second (dt : PlainDateTime) : Second.Ordinal dt.time.second.fst :=
-  dt.time.second.snd
+def second (dt : PlainDateTime) : Second.Ordinal dt.time.fst :=
+  dt.time.snd.second
 
 /--
 Getter for the `Nanosecond.Ordinal` inside of a `PlainDateTime`.
 -/
 @[inline]
 def nanosecond (dt : PlainDateTime) : Nanosecond.Ordinal :=
-  dt.time.nanosecond
+  dt.time.snd.nanosecond
 
 /--
 Determines the era of the given `PlainDateTime` based on its year.
@@ -521,15 +528,15 @@ def quarter (date : PlainDateTime) : Bounded.LE 1 4 :=
 Combines a `PlainDate` and `PlainTime` into a `PlainDateTime`.
 -/
 @[inline]
-def atTime : PlainDate → PlainTime → PlainDateTime :=
-  PlainDateTime.mk
+def atTime : PlainDate → PlainTime leap → PlainDateTime :=
+  (PlainDateTime.mk · <| Sigma.mk leap ·)
 
 /--
 Combines a `PlainTime` and `PlainDate` into a `PlainDateTime`.
 -/
 @[inline]
-def atDate (time: PlainTime) (date: PlainDate) : PlainDateTime :=
-  PlainDateTime.mk date time
+def atDate (time: PlainTime leap) (date: PlainDate) : PlainDateTime :=
+  PlainDateTime.mk date (Sigma.mk leap time)
 
 instance : HAdd PlainDateTime Day.Offset PlainDateTime where
   hAdd := addDays
@@ -583,8 +590,8 @@ namespace PlainDate
 Combines a `PlainDate` and `PlainTime` into a `PlainDateTime`.
 -/
 @[inline]
-def atTime : PlainDate → PlainTime → PlainDateTime :=
-  PlainDateTime.mk
+def atTime : PlainDate → PlainTime leap → PlainDateTime :=
+  (PlainDateTime.mk · <| Sigma.mk leap ·)
 
 end PlainDate
 namespace PlainTime
@@ -593,8 +600,8 @@ namespace PlainTime
 Combines a `PlainTime` and `PlainDate` into a `PlainDateTime`.
 -/
 @[inline]
-def atDate (time: PlainTime) (date: PlainDate) : PlainDateTime :=
-  PlainDateTime.mk date time
+def atDate (time: PlainTime leap) (date: PlainDate) : PlainDateTime :=
+  PlainDateTime.mk date (Sigma.mk leap time)
 
 end PlainTime
 end Time
diff --git a/src/Std/Time/DateTime/Timestamp.lean b/src/Std/Time/DateTime/Timestamp.lean
index 8ba43cc11892..ff503ce59819 100644
--- a/src/Std/Time/DateTime/Timestamp.lean
+++ b/src/Std/Time/DateTime/Timestamp.lean
@@ -38,10 +38,10 @@ instance : OfNat Timestamp n where
   ofNat := ⟨OfNat.ofNat n⟩
 
 instance : ToString Timestamp where
-  toString s := toString s.val.toMilliseconds
+  toString s := toString s.val.toSeconds
 
 instance : Repr Timestamp where
-  reprPrec s := reprPrec (toString s)
+  reprPrec s := reprPrec s.val.toSeconds
 
 namespace Timestamp
 
diff --git a/src/Std/Time/Duration.lean b/src/Std/Time/Duration.lean
index 54d6d0364340..51f828cca906 100644
--- a/src/Std/Time/Duration.lean
+++ b/src/Std/Time/Duration.lean
@@ -350,10 +350,10 @@ instance : HMul Int Duration Duration where
 instance : HMul Duration Int Duration where
   hMul d i := Duration.ofNanoseconds <| Nanosecond.Offset.ofInt (d.toNanoseconds.val * i)
 
-instance : HAdd PlainTime Duration PlainTime where
+instance : HAdd (PlainTime leap) Duration (PlainTime leap) where
    hAdd pt d := PlainTime.ofNanoseconds (d.toNanoseconds + pt.toNanoseconds)
 
-instance : HSub PlainTime Duration PlainTime where
+instance : HSub (PlainTime leap) Duration (PlainTime leap) where
    hSub pt d := PlainTime.ofNanoseconds (d.toNanoseconds - pt.toNanoseconds)
 
 end Duration
diff --git a/src/Std/Time/Format.lean b/src/Std/Time/Format.lean
index 6d4b31c3af37..1345fb368070 100644
--- a/src/Std/Time/Format.lean
+++ b/src/Std/Time/Format.lean
@@ -254,7 +254,7 @@ namespace PlainTime
 /--
 Formats a `PlainTime` using a specific format.
 -/
-def format (time : PlainTime) (format : String) : String :=
+def format (time : PlainTime leap) (format : String) : String :=
   let format : Except String (GenericFormat .any) := GenericFormat.spec format
   match format with
   | .error err => s!"error: {err}"
@@ -264,7 +264,7 @@ def format (time : PlainTime) (format : String) : String :=
       | .k _ => some (time.hour.shiftTo1BasedHour)
       | .m _ => some time.minute
       | .n _ => some time.nanosecond
-      | .s _ => some time.second
+      | .s _ => some (Sigma.mk leap time.second)
       | .a _ => some (HourMarker.ofOrdinal time.hour)
       | .h _ => some time.hour.toRelative
       | .K _ => some (time.hour.emod 12 (by decide))
@@ -279,55 +279,55 @@ def format (time : PlainTime) (format : String) : String :=
 /--
 Parses a time string in the 24-hour format (`HH:mm:ss`) and returns a `PlainTime`.
 -/
-def fromTime24Hour (input : String) : Except String PlainTime :=
-  Formats.time24Hour.parseBuilder (fun h m s => some (PlainTime.ofHourMinuteSeconds h m s.snd)) input
+def fromTime24Hour (input : String) : Except String (Sigma PlainTime) :=
+  Formats.time24Hour.parseBuilder (fun h m s => some (Sigma.mk s.fst (PlainTime.ofHourMinuteSeconds h m s.snd))) input
 
 /--
 Formats a `PlainTime` value into a 24-hour format string (`HH:mm:ss`).
 -/
-def toTime24Hour (input : PlainTime) : String :=
-  Formats.time24Hour.formatBuilder input.hour input.minute input.second
+def toTime24Hour (input : PlainTime leap) : String :=
+  Formats.time24Hour.formatBuilder input.hour input.minute (Sigma.mk leap input.second)
 
 /--
 Parses a time string in the lean 24-hour format (`HH:mm:ss.SSSSSSSSS` or `HH:mm:ss`) and returns a `PlainTime`.
 -/
-def fromLeanTime24Hour (input : String) : Except String PlainTime :=
-  Formats.leanTime24Hour.parseBuilder (fun h m s n => some (PlainTime.ofHourMinuteSecondsNano h m s.snd n)) input
-  <|> Formats.leanTime24HourNoNanos.parseBuilder (fun h m s => some (PlainTime.ofHourMinuteSecondsNano h m s.snd 0)) input
+def fromLeanTime24Hour (input : String) : Except String (Sigma PlainTime) :=
+  Formats.leanTime24Hour.parseBuilder (fun h m s n => some <| Sigma.mk s.fst (PlainTime.ofHourMinuteSecondsNano h m s.snd n)) input
+  <|> Formats.leanTime24HourNoNanos.parseBuilder (fun h m s => some <| Sigma.mk s.fst (PlainTime.ofHourMinuteSecondsNano h m s.snd 0)) input
 
 /--
 Formats a `PlainTime` value into a 24-hour format string (`HH:mm:ss.SSSSSSSSS`).
 -/
-def toLeanTime24Hour (input : PlainTime) : String :=
-  Formats.leanTime24Hour.formatBuilder input.hour input.minute input.second input.nanosecond
+def toLeanTime24Hour (input : PlainTime leap) : String :=
+  Formats.leanTime24Hour.formatBuilder input.hour input.minute (Sigma.mk leap input.second) input.nanosecond
 
 /--
 Parses a time string in the 12-hour format (`hh:mm:ss aa`) and returns a `PlainTime`.
 -/
-def fromTime12Hour (input : String) : Except String PlainTime := do
-  let builder h m s a : Option PlainTime := do
+def fromTime12Hour (input : String) : Except String (Sigma PlainTime) := do
+  let builder h m s a : Option (Sigma PlainTime) := do
     let value ← Internal.Bounded.ofInt? h.val
-    some <| PlainTime.ofHourMinuteSeconds (HourMarker.toAbsolute a value) m s.snd
+    some <| Sigma.mk s.fst <| PlainTime.ofHourMinuteSeconds (HourMarker.toAbsolute a value) m s.snd
 
   Formats.time12Hour.parseBuilder builder input
 
 /--
 Formats a `PlainTime` value into a 12-hour format string (`hh:mm:ss aa`).
 -/
-def toTime12Hour (input : PlainTime) : String :=
-  Formats.time12Hour.formatBuilder (input.hour.emod 12 (by decide) |>.add 1) input.minute input.second (if input.hour.val ≥ 12 then HourMarker.pm else HourMarker.am)
+def toTime12Hour (input : PlainTime leap) : String :=
+  Formats.time12Hour.formatBuilder (input.hour.emod 12 (by decide) |>.add 1) input.minute (Sigma.mk leap input.second) (if input.hour.val ≥ 12 then HourMarker.pm else HourMarker.am)
 
 /--
 Parses a `String` in the `Time12Hour` or `Time24Hour` format and returns a `PlainTime`.
 -/
-def parse (input : String) : Except String PlainTime :=
+def parse (input : String) : Except String (Sigma PlainTime) :=
   fromTime12Hour input
   <|> fromTime24Hour input
 
-instance : ToString PlainTime where
+instance : ToString (PlainTime leap) where
   toString := toLeanTime24Hour
 
-instance : Repr PlainTime where
+instance : Repr (PlainTime leap) where
   reprPrec data := Repr.addAppParen ("time(\"" ++ toLeanTime24Hour data ++ "\")")
 
 end PlainTime
@@ -409,12 +409,12 @@ def fromLeanDateTimeWithIdentifierString (input : String) : Except String ZonedD
 Formats a `DateTime` value into a simple date time with timezone string that can be parsed by the date% notation.
 -/
 def toLeanDateTimeWithZoneString (zdt : ZonedDateTime) : String :=
-  Formats.leanDateTimeWithZone.formatBuilder zdt.year zdt.month zdt.day zdt.hour zdt.minute zdt.date.get.time.second zdt.nanosecond zdt.offset
+  Formats.leanDateTimeWithZone.formatBuilder zdt.year zdt.month zdt.day zdt.hour zdt.minute (Sigma.mk zdt.date.get.time.fst zdt.date.get.time.snd.second) zdt.nanosecond zdt.offset
 /--
 Formats a `DateTime` value into a simple date time with timezone string that can be parsed by the date% notation with the timezone identifier.
 -/
 def toLeanDateTimeWithIdentifierString (zdt : ZonedDateTime) : String :=
-  Formats.leanDateTimeWithIdentifierAndNanos.formatBuilder zdt.year zdt.month zdt.day zdt.hour zdt.minute zdt.date.get.time.second zdt.nanosecond zdt.timezone.name
+  Formats.leanDateTimeWithIdentifierAndNanos.formatBuilder zdt.year zdt.month zdt.day zdt.hour zdt.minute (Sigma.mk zdt.date.get.time.fst zdt.date.get.time.snd.second) zdt.nanosecond zdt.timezone.name
 
 /--
 Parses a `String` in the `ISO8601`, `RFC822` or `RFC850` format and returns a `ZonedDateTime`.
@@ -461,13 +461,13 @@ def format (date : PlainDateTime) (format : String) : String :=
       | .k _ => some date.hour.shiftTo1BasedHour
       | .m _ => some date.minute
       | .n _ => some date.nanosecond
-      | .s _ => some date.time.second
+      | .s _ => some (Sigma.mk date.time.fst date.time.snd.second)
       | .a _ => some (HourMarker.ofOrdinal date.hour)
       | .h _ => some date.hour.toRelative
       | .K _ => some (date.hour.emod 12 (by decide))
       | .S _ => some date.nanosecond
-      | .A _ => some date.time.toMilliseconds
-      | .N _ => some date.time.toNanoseconds
+      | .A _ => some date.time.snd.toMilliseconds
+      | .N _ => some date.time.snd.toNanoseconds
       | _ => none
     match res with
     | some res => res
@@ -510,7 +510,7 @@ def fromDateTimeString (input : String) : Except String PlainDateTime :=
 Formats a `PlainDateTime` value into a `DateTime` format string.
 -/
 def toDateTimeString (pdt : PlainDateTime) : String :=
-  Formats.dateTime24Hour.formatBuilder pdt.year pdt.month pdt.day pdt.hour pdt.minute pdt.time.second pdt.nanosecond
+  Formats.dateTime24Hour.formatBuilder pdt.year pdt.month pdt.day pdt.hour pdt.minute (Sigma.mk pdt.time.fst pdt.time.snd.second) pdt.nanosecond
 
 /--
 Parses a `String` in the `DateTime` format and returns a `PlainDateTime`.
@@ -523,7 +523,7 @@ def fromLeanDateTimeString (input : String) : Except String PlainDateTime :=
 Formats a `PlainDateTime` value into a `DateTime` format string.
 -/
 def toLeanDateTimeString (pdt : PlainDateTime) : String :=
-  Formats.leanDateTime24Hour.formatBuilder pdt.year pdt.month pdt.day pdt.hour pdt.minute pdt.time.second pdt.nanosecond
+  Formats.leanDateTime24Hour.formatBuilder pdt.year pdt.month pdt.day pdt.hour pdt.minute (Sigma.mk pdt.time.fst pdt.time.snd.second) pdt.nanosecond
 
 /--
 Parses a `String` in the `AscTime` or `LongDate` format and returns a `PlainDateTime`.
diff --git a/src/Std/Time/Format/Basic.lean b/src/Std/Time/Format/Basic.lean
index 0ecde2581c55..b3941bb446ee 100644
--- a/src/Std/Time/Format/Basic.lean
+++ b/src/Std/Time/Format/Basic.lean
@@ -736,12 +736,12 @@ private def toSigned (data : Int) : String :=
 
 private def toIsoString (offset : Offset) (withMinutes : Bool) (withSeconds : Bool) (colon : Bool) : String :=
   let (sign, time) := if offset.second.val ≥ 0 then ("+", offset.second) else ("-", -offset.second)
-  let time := PlainTime.ofSeconds time
+  let time : LeapTime := PlainTime.ofSeconds time
   let pad := leftPad 2 '0' ∘ toString
 
   let data := s!"{sign}{pad time.hour.val}"
   let data := if withMinutes then s!"{data}{if colon then ":" else ""}{pad time.minute.val}" else data
-  let data := if withSeconds ∧ time.second.snd.val ≠ 0 then s!"{data}{if colon then ":" else ""}{pad time.second.snd.val}" else data
+  let data := if withSeconds ∧ time.second.val ≠ 0 then s!"{data}{if colon then ":" else ""}{pad time.second.val}" else data
 
   data
 
@@ -913,11 +913,11 @@ private def dateFromModifier (date : DateTime tz) : TypeFormat modifier :=
   | .k _ => date.hour.shiftTo1BasedHour
   | .H _ => date.hour
   | .m _ => date.minute
-  | .s _ => date.date.get.time.second
+  | .s _ => Sigma.mk date.date.get.time.fst date.date.get.time.snd.second
   | .S _ => date.nanosecond
-  | .A _ => date.date.get.time.toMilliseconds
+  | .A _ => date.date.get.time.snd.toMilliseconds
   | .n _ => date.nanosecond
-  | .N _ => date.date.get.time.toNanoseconds
+  | .N _ => date.date.get.time.snd.toNanoseconds
   | .V => tz.name
   | .z .short => tz.abbreviation
   | .z .full => tz.name
@@ -1338,15 +1338,15 @@ private def build (builder : DateBuilder) (aw : Awareness) : Option aw.type :=
   let second := builder.s |>.getD ⟨false, 0⟩
   let nano := (builder.n <|> builder.S) |>.getD 0
 
-  let time : PlainTime
+  let time : PlainTime second.fst
     :=  PlainTime.ofNanoseconds <$> builder.N
     <|> PlainTime.ofMilliseconds <$> builder.A
-    |>.getD (PlainTime.mk hour minute second nano)
+    |>.getD (PlainTime.mk hour minute second.snd nano)
 
   let datetime : Option PlainDateTime :=
     if valid : year.Valid month day then
       let date : PlainDate := { year, month, day, valid }
-      some { date, time }
+      some { date, time := Sigma.mk second.fst time }
     else
       none
 
diff --git a/src/Std/Time/Notation.lean b/src/Std/Time/Notation.lean
index b8b5e35bcfdb..bdf39a69e834 100644
--- a/src/Std/Time/Notation.lean
+++ b/src/Std/Time/Notation.lean
@@ -125,11 +125,11 @@ private def convertTimezone (tz : Std.Time.TimeZone) : MacroM (TSyntax `term) :=
 private def convertPlainDate (d : Std.Time.PlainDate) : MacroM (TSyntax `term) := do
  `(Std.Time.PlainDate.ofYearMonthDayClip $(← syntaxInt d.year) $(← syntaxBounded d.month.val) $(← syntaxBounded d.day.val))
 
-private def convertPlainTime (d : Std.Time.PlainTime) : MacroM (TSyntax `term) := do
- `(Std.Time.PlainTime.mk $(← syntaxBounded d.hour.val) $(← syntaxBounded d.minute.val) ⟨true, $(← syntaxBounded d.second.snd.val)⟩ $(← syntaxBounded d.nanosecond.val))
+private def convertPlainTime (d : Std.Time.PlainTime leap) : MacroM (TSyntax `term) := do
+ `(Std.Time.PlainTime.mk $(← syntaxBounded d.hour.val) $(← syntaxBounded d.minute.val) $(← syntaxBounded d.second.val) $(← syntaxBounded d.nanosecond.val))
 
 private def convertPlainDateTime (d : Std.Time.PlainDateTime) : MacroM (TSyntax `term) := do
- `(Std.Time.PlainDateTime.mk $(← convertPlainDate d.date) $(← convertPlainTime d.time))
+ `(Std.Time.PlainDateTime.mk $(← convertPlainDate d.date) (Sigma.mk true $(← convertPlainTime (d.time.snd))))
 
 private def convertZonedDateTime (d : Std.Time.ZonedDateTime) (identifier := false) : MacroM (TSyntax `term) := do
   let plain ← convertPlainDateTime d.toPlainDateTime
@@ -232,7 +232,7 @@ macro_rules
 
   | `(time( $time:str )) => do
       match PlainTime.fromLeanTime24Hour time.getString with
-      | .ok res => return ← convertPlainTime res
+      | .ok res => return ← convertPlainTime res.snd
       | .error res => Macro.throwErrorAt time s!"error: {res}"
 
   | `(offset( $offset:str )) => do
diff --git a/src/Std/Time/Time/PlainTime.lean b/src/Std/Time/Time/PlainTime.lean
index 3c0b2d3e0061..7ce514c801d7 100644
--- a/src/Std/Time/Time/PlainTime.lean
+++ b/src/Std/Time/Time/PlainTime.lean
@@ -15,7 +15,7 @@ set_option linter.all true
 /--
 Represents a specific point in a day, including hours, minutes, seconds, and nanoseconds.
 -/
-structure PlainTime where
+structure PlainTime (leap : Bool) where
 
   /--
   `Hour` component of the `PlainTime`
@@ -30,7 +30,7 @@ structure PlainTime where
   /--
   `Second` component of the `PlainTime`
   -/
-  second : Sigma Second.Ordinal
+  second : Second.Ordinal leap
 
   /--
   `Nanoseconds` component of the `PlainTime`
@@ -38,120 +38,132 @@ structure PlainTime where
   nanosecond : Nanosecond.Ordinal
   deriving Repr
 
-instance : Inhabited PlainTime where
-  default := ⟨0, 0, Sigma.mk false 0, 0, by decide⟩
+/--
+Defines `LeapTime` as a shorthand for a `PlainTime` that can contain leap seconds.
+-/
+abbrev LeapTime := PlainTime true
+
+instance : Inhabited (PlainTime x) where
+  default := ⟨0, 0, 0, 0, by decide⟩
 
-instance : BEq PlainTime where
+instance : BEq (PlainTime x) where
   beq x y := x.hour.val == y.hour.val && x.minute == y.minute
-          && x.second.snd.val == y.second.snd.val && x.nanosecond == y.nanosecond
+          && x.second.val == y.second.val && x.nanosecond == y.nanosecond
 
 namespace PlainTime
 
 /--
 Creates a `PlainTime` value representing midnight (00:00:00.000000000).
 -/
-def midnight : PlainTime :=
-  ⟨0, 0, ⟨true, 0⟩, 0⟩
+def midnight : PlainTime leap :=
+  ⟨0, 0, 0, 0⟩
 
 /--
 Creates a `PlainTime` value from the provided hours, minutes, seconds and nanoseconds components.
 -/
 @[inline]
-def ofHourMinuteSecondsNano (hour : Hour.Ordinal) (minute : Minute.Ordinal) (second : Second.Ordinal leap) (nano : Nanosecond.Ordinal) : PlainTime :=
-  ⟨hour, minute, Sigma.mk leap second, nano⟩
+def ofHourMinuteSecondsNano (hour : Hour.Ordinal) (minute : Minute.Ordinal) (second : Second.Ordinal leap) (nano : Nanosecond.Ordinal) : PlainTime leap :=
+  ⟨hour, minute, second, nano⟩
 
 /--
 Creates a `PlainTime` value from the provided hours, minutes, and seconds.
 -/
 @[inline]
-def ofHourMinuteSeconds (hour : Hour.Ordinal) (minute : Minute.Ordinal) (second : Second.Ordinal leap) : PlainTime :=
+def ofHourMinuteSeconds (hour : Hour.Ordinal) (minute : Minute.Ordinal) (second : Second.Ordinal leap) : PlainTime leap :=
   ofHourMinuteSecondsNano hour minute second 0
 
 /--
 Converts a `PlainTime` value to the total number of milliseconds.
 -/
-def toMilliseconds (time : PlainTime) : Millisecond.Offset :=
+def toMilliseconds (time : PlainTime leap) : Millisecond.Offset :=
   time.hour.toOffset.toMilliseconds +
   time.minute.toOffset.toMilliseconds +
-  time.second.snd.toOffset.toMilliseconds +
+  time.second.toOffset.toMilliseconds +
   time.nanosecond.toOffset.toMilliseconds
 
 /--
 Converts a `PlainTime` value to the total number of nanoseconds.
 -/
-def toNanoseconds (time : PlainTime) : Nanosecond.Offset :=
+def toNanoseconds (time : PlainTime leap) : Nanosecond.Offset :=
   time.hour.toOffset.toNanoseconds +
   time.minute.toOffset.toNanoseconds +
-  time.second.snd.toOffset.toNanoseconds +
+  time.second.toOffset.toNanoseconds +
   time.nanosecond.toOffset
 
 /--
 Converts a `PlainTime` value to the total number of seconds.
 -/
-def toSeconds (time : PlainTime) : Second.Offset :=
+def toSeconds (time : PlainTime leap) : Second.Offset :=
   time.hour.toOffset.toSeconds +
   time.minute.toOffset.toSeconds +
-  time.second.snd.toOffset
+  time.second.toOffset
 
 /--
 Converts a `PlainTime` value to the total number of minutes.
 -/
-def toMinutes (time : PlainTime) : Minute.Offset :=
+def toMinutes (time : PlainTime leap) : Minute.Offset :=
   time.hour.toOffset.toMinutes +
   time.minute.toOffset +
-  time.second.snd.toOffset.toMinutes
+  time.second.toOffset.toMinutes
 
 /--
 Converts a `PlainTime` value to the total number of hours.
 -/
-def toHours (time : PlainTime) : Hour.Offset :=
+def toHours (time : PlainTime leap) : Hour.Offset :=
   time.hour.toOffset
 
 /--
 Creates a `PlainTime` value from a total number of nanoseconds.
 -/
-def ofNanoseconds (nanos : Nanosecond.Offset) : PlainTime :=
+def ofNanoseconds (nanos : Nanosecond.Offset) : PlainTime leap :=
   have totalSeconds := nanos.ediv 1000000000
   have remainingNanos := Bounded.LE.byEmod nanos.val 1000000000 (by decide)
   have hours := Bounded.LE.byEmod (totalSeconds.val / 3600) 24 (by decide)
   have minutes := (Bounded.LE.byEmod totalSeconds.val 3600 (by decide)).ediv 60 (by decide)
+
   have seconds := Bounded.LE.byEmod totalSeconds.val 60 (by decide)
+
+  have seconds :=
+    match leap with
+    | true => seconds.expandTop (by decide)
+    | false => seconds
+
   let nanos := Bounded.LE.byEmod nanos.val 1000000000 (by decide)
-  PlainTime.mk hours minutes (Sigma.mk false seconds) nanos
+  PlainTime.mk hours minutes seconds nanos
 
 /--
 Creates a `PlainTime` value from a total number of millisecond.
 -/
 @[inline]
-def ofMilliseconds (millis : Millisecond.Offset) : PlainTime :=
+def ofMilliseconds (millis : Millisecond.Offset) : PlainTime leap :=
   ofNanoseconds millis.toNanoseconds
 
 /--
 Creates a `PlainTime` value from a total number of seconds.
 -/
 @[inline]
-def ofSeconds (secs : Second.Offset) : PlainTime :=
+def ofSeconds (secs : Second.Offset) : PlainTime leap :=
   ofNanoseconds secs.toNanoseconds
 
 /--
 Creates a `PlainTime` value from a total number of minutes.
 -/
 @[inline]
-def ofMinutes (secs : Minute.Offset) : PlainTime :=
+def ofMinutes (secs : Minute.Offset) : PlainTime leap :=
   ofNanoseconds secs.toNanoseconds
 
 /--
 Creates a `PlainTime` value from a total number of hours.
 -/
 @[inline]
-def ofHours (hour : Hour.Offset) : PlainTime :=
+def ofHours (hour : Hour.Offset) : PlainTime leap :=
   ofNanoseconds hour.toNanoseconds
 
 /--
 Adds seconds to a `PlainTime`.
 -/
 @[inline]
-def addSeconds (time : PlainTime) (secondsToAdd : Second.Offset) : PlainTime :=
+def addSeconds (time : PlainTime leap) (secondsToAdd : Second.Offset) : PlainTime leap :=
   let totalSeconds := time.toNanoseconds + secondsToAdd.toNanoseconds
   ofNanoseconds totalSeconds
 
@@ -159,14 +171,14 @@ def addSeconds (time : PlainTime) (secondsToAdd : Second.Offset) : PlainTime :=
 Subtracts seconds from a `PlainTime`.
 -/
 @[inline]
-def subSeconds (time : PlainTime) (secondsToSub : Second.Offset) : PlainTime :=
+def subSeconds (time : PlainTime leap) (secondsToSub : Second.Offset) : PlainTime leap :=
   addSeconds time (-secondsToSub)
 
 /--
 Adds minutes to a `PlainTime`.
 -/
 @[inline]
-def addMinutes (time : PlainTime) (minutesToAdd : Minute.Offset) : PlainTime :=
+def addMinutes (time : PlainTime leap) (minutesToAdd : Minute.Offset) : PlainTime leap :=
   let total := time.toNanoseconds + minutesToAdd.toNanoseconds
   ofNanoseconds total
 
@@ -174,14 +186,14 @@ def addMinutes (time : PlainTime) (minutesToAdd : Minute.Offset) : PlainTime :=
 Subtracts minutes from a `PlainTime`.
 -/
 @[inline]
-def subMinutes (time : PlainTime) (minutesToSub : Minute.Offset) : PlainTime :=
+def subMinutes (time : PlainTime leap) (minutesToSub : Minute.Offset) : PlainTime leap :=
   addMinutes time (-minutesToSub)
 
 /--
 Adds hours to a `PlainTime`.
 -/
 @[inline]
-def addHours (time : PlainTime) (hoursToAdd : Hour.Offset) : PlainTime :=
+def addHours (time : PlainTime leap) (hoursToAdd : Hour.Offset) : PlainTime leap :=
   let total := time.toNanoseconds + hoursToAdd.toNanoseconds
   ofNanoseconds total
 
@@ -189,54 +201,54 @@ def addHours (time : PlainTime) (hoursToAdd : Hour.Offset) : PlainTime :=
 Subtracts hours from a `PlainTime`.
 -/
 @[inline]
-def subHours (time : PlainTime) (hoursToSub : Hour.Offset) : PlainTime :=
+def subHours (time : PlainTime leap) (hoursToSub : Hour.Offset) : PlainTime leap :=
   addHours time (-hoursToSub)
 
 /--
 Adds nanoseconds to a `PlainTime`.
 -/
-def addNanoseconds (time : PlainTime) (nanosToAdd : Nanosecond.Offset) : PlainTime :=
+def addNanoseconds (time : PlainTime leap) (nanosToAdd : Nanosecond.Offset) : PlainTime leap :=
   let total := time.toNanoseconds + nanosToAdd
   ofNanoseconds total
 
 /--
 Subtracts nanoseconds from a `PlainTime`.
 -/
-def subNanoseconds (time : PlainTime) (nanosToSub : Nanosecond.Offset) : PlainTime :=
+def subNanoseconds (time : PlainTime leap) (nanosToSub : Nanosecond.Offset) : PlainTime leap :=
   addNanoseconds time (-nanosToSub)
 
 /--
 Adds milliseconds to a `PlainTime`.
 -/
-def addMilliseconds (time : PlainTime) (millisToAdd : Millisecond.Offset) : PlainTime :=
+def addMilliseconds (time : PlainTime leap) (millisToAdd : Millisecond.Offset) : PlainTime leap :=
   let total := time.toMilliseconds + millisToAdd
   ofMilliseconds total
 
 /--
 Subtracts milliseconds from a `PlainTime`.
 -/
-def subMilliseconds (time : PlainTime) (millisToSub : Millisecond.Offset) : PlainTime :=
+def subMilliseconds (time : PlainTime leap) (millisToSub : Millisecond.Offset) : PlainTime leap :=
   addMilliseconds time (-millisToSub)
 
 /--
 Creates a new `PlainTime` by adjusting the `second` component to the given value.
 -/
 @[inline]
-def withSeconds (pt : PlainTime) (second : Sigma Second.Ordinal) : PlainTime :=
+def withSeconds (pt : PlainTime leap) (second : Second.Ordinal leap) : PlainTime leap :=
   { pt with second := second }
 
 /--
 Creates a new `PlainTime` by adjusting the `minute` component to the given value.
 -/
 @[inline]
-def withMinutes (pt : PlainTime) (minute : Minute.Ordinal) : PlainTime :=
+def withMinutes (pt : PlainTime leap) (minute : Minute.Ordinal) : PlainTime leap :=
   { pt with minute := minute }
 
 /--
 Creates a new `PlainTime` by adjusting the milliseconds component inside the `nano` component of its `time` to the given value.
 -/
 @[inline]
-def withMilliseconds (pt : PlainTime) (millis : Millisecond.Ordinal) : PlainTime :=
+def withMilliseconds (pt : PlainTime leap) (millis : Millisecond.Ordinal) : PlainTime leap :=
   let minorPart := pt.nanosecond.emod 1000 (by decide)
   let majorPart := millis.mul_pos 1000000 (by decide) |>.addBounds minorPart
   { pt with nanosecond := majorPart |>.expandTop (by decide) }
@@ -245,51 +257,51 @@ def withMilliseconds (pt : PlainTime) (millis : Millisecond.Ordinal) : PlainTime
 Creates a new `PlainTime` by adjusting the `nano` component to the given value.
 -/
 @[inline]
-def withNanoseconds (pt : PlainTime) (nano : Nanosecond.Ordinal) : PlainTime :=
+def withNanoseconds (pt : PlainTime leap) (nano : Nanosecond.Ordinal) : PlainTime leap :=
   { pt with nanosecond := nano }
 
 /--
 Creates a new `PlainTime` by adjusting the `hour` component to the given value.
 -/
 @[inline]
-def withHours (pt : PlainTime) (hour : Hour.Ordinal) : PlainTime :=
+def withHours (pt : PlainTime leap) (hour : Hour.Ordinal) : PlainTime leap :=
   { pt with hour := hour }
 
 /--
 `Millisecond` component of the `PlainTime`
 -/
 @[inline]
-def millisecond (pt : PlainTime) : Millisecond.Ordinal :=
+def millisecond (pt : PlainTime leap) : Millisecond.Ordinal :=
   pt.nanosecond.ediv 1000000 (by decide)
 
-instance : HAdd PlainTime Nanosecond.Offset PlainTime where
+instance : HAdd (PlainTime leap) Nanosecond.Offset (PlainTime leap) where
   hAdd := addNanoseconds
 
-instance : HSub PlainTime Nanosecond.Offset PlainTime where
+instance : HSub (PlainTime leap) Nanosecond.Offset (PlainTime leap) where
   hSub := subNanoseconds
 
-instance : HAdd PlainTime Millisecond.Offset PlainTime where
+instance : HAdd (PlainTime leap) Millisecond.Offset (PlainTime leap) where
   hAdd := addMilliseconds
 
-instance : HSub PlainTime Millisecond.Offset PlainTime where
+instance : HSub (PlainTime leap) Millisecond.Offset (PlainTime leap) where
   hSub := subMilliseconds
 
-instance : HAdd PlainTime Second.Offset PlainTime where
+instance : HAdd (PlainTime leap) Second.Offset (PlainTime leap) where
   hAdd := addSeconds
 
-instance : HSub PlainTime Second.Offset PlainTime where
+instance : HSub (PlainTime leap) Second.Offset (PlainTime leap) where
   hSub := subSeconds
 
-instance : HAdd PlainTime Minute.Offset PlainTime where
+instance : HAdd (PlainTime leap) Minute.Offset (PlainTime leap) where
   hAdd := addMinutes
 
-instance : HSub PlainTime Minute.Offset PlainTime where
+instance : HSub (PlainTime leap) Minute.Offset (PlainTime leap) where
   hSub := subMinutes
 
-instance : HAdd PlainTime Hour.Offset PlainTime where
+instance : HAdd (PlainTime leap) Hour.Offset (PlainTime leap) where
   hAdd := addHours
 
-instance : HSub PlainTime Hour.Offset PlainTime where
+instance : HSub (PlainTime leap) Hour.Offset (PlainTime leap) where
   hSub := subHours
 
 end PlainTime
diff --git a/src/Std/Time/Zoned.lean b/src/Std/Time/Zoned.lean
index 570007ce5ecb..e1500adc6784 100644
--- a/src/Std/Time/Zoned.lean
+++ b/src/Std/Time/Zoned.lean
@@ -45,8 +45,9 @@ namespace PlainTime
 Get the current time.
 -/
 @[inline]
-def now : IO PlainTime :=
-  PlainDateTime.time <$> PlainDateTime.now
+def now : IO (Sigma PlainTime) := do
+  let res ← PlainDateTime.time <$> PlainDateTime.now
+  return res
 
 end PlainTime
 
@@ -70,8 +71,8 @@ def toPlainDate (dt : DateTime tz) : PlainDate :=
 Converts a `DateTime` to a `PlainTime`
 -/
 @[inline]
-def toPlainTime (dt : DateTime tz) : PlainTime :=
-  dt.date.get.time
+def toPlainTime (dt : DateTime tz) : PlainTime dt.date.get.time.fst :=
+  dt.date.get.time.snd
 
 end DateTime
 namespace DateTime
@@ -110,14 +111,14 @@ Converts a `PlainDate` to a `ZonedDateTime`.
 -/
 @[inline]
 def ofPlainDate (pd : PlainDate) (zr : TimeZone.ZoneRules) : ZonedDateTime :=
-  ZonedDateTime.ofPlainDateTime (pd.atTime PlainTime.midnight) zr
+  ZonedDateTime.ofPlainDateTime (pd.atTime (leap := true) PlainTime.midnight) zr
 
 /--
 Converts a `PlainDate` to a `ZonedDateTime` using `TimeZone`.
 -/
 @[inline]
 def ofPlainDateWithZone (pd : PlainDate) (zr : TimeZone) : ZonedDateTime :=
-  ZonedDateTime.ofPlainDateTime (pd.atTime PlainTime.midnight) (TimeZone.ZoneRules.ofTimeZone zr)
+  ZonedDateTime.ofPlainDateTime (pd.atTime (leap := true) PlainTime.midnight) (TimeZone.ZoneRules.ofTimeZone zr)
 
 /--
 Converts a `ZonedDateTime` to a `PlainDate`
@@ -130,7 +131,7 @@ def toPlainDate (dt : ZonedDateTime) : PlainDate :=
 Converts a `ZonedDateTime` to a `PlainTime`
 -/
 @[inline]
-def toPlainTime (dt : ZonedDateTime) : PlainTime :=
+def toPlainTime (dt : ZonedDateTime) : Sigma PlainTime :=
   dt.toPlainDateTime.time
 
 /--
diff --git a/src/Std/Time/Zoned/Database/TZdb.lean b/src/Std/Time/Zoned/Database/TZdb.lean
index 5c0d49bafbad..4a5ebd2deb37 100644
--- a/src/Std/Time/Zoned/Database/TZdb.lean
+++ b/src/Std/Time/Zoned/Database/TZdb.lean
@@ -71,12 +71,7 @@ def idFromPath (path : System.FilePath) : Option String := do
 Retrieves the timezone rules from the local timezone data file.
 -/
 def localRules (path : System.FilePath) : IO ZoneRules := do
-  let localTimePath ←
-    try
-      IO.Process.run { cmd := "readlink", args := #["-f", path.toString] }
-    catch _ =>
-      throw <| IO.userError "cannot find the local timezone database"
-
+  let localTimePath ← IO.FS.realPath path
   if let some id := idFromPath localTimePath
     then parseTZIfFromDisk path id
     else throw (IO.userError "cannot read the id of the path.")
diff --git a/src/Std/Time/Zoned/DateTime.lean b/src/Std/Time/Zoned/DateTime.lean
index 4f69cda6ce62..2a743b921e7c 100644
--- a/src/Std/Time/Zoned/DateTime.lean
+++ b/src/Std/Time/Zoned/DateTime.lean
@@ -305,7 +305,7 @@ def withMinutes (dt : DateTime tz) (minute : Minute.Ordinal) : DateTime tz :=
 Creates a new `DateTime tz` by adjusting the `second` component.
 -/
 @[inline]
-def withSeconds (dt : DateTime tz) (second : Sigma Second.Ordinal) : DateTime tz :=
+def withSeconds (dt : DateTime tz) (second : Second.Ordinal α) : DateTime tz :=
   ofPlainDateTime (dt.date.get.withSeconds second) tz
 
 /--
@@ -368,7 +368,7 @@ def minute (dt : DateTime tz) : Minute.Ordinal :=
 Getter for the `Second` inside of a `DateTime`
 -/
 @[inline]
-def second (dt : DateTime tz) : Second.Ordinal dt.date.get.time.second.fst :=
+def second (dt : DateTime tz) : Second.Ordinal dt.date.get.time.fst :=
   dt.date.get.second
 
 /--
@@ -376,14 +376,14 @@ Getter for the `Milliseconds` inside of a `DateTime`
 -/
 @[inline]
 def millisecond (dt : DateTime tz) : Millisecond.Ordinal :=
-  dt.date.get.time.nanosecond.emod 1000 (by decide)
+  dt.date.get.time.snd.nanosecond.emod 1000 (by decide)
 
 /--
 Getter for the `Nanosecond` inside of a `DateTime`
 -/
 @[inline]
 def nanosecond (dt : DateTime tz) : Nanosecond.Ordinal :=
-  dt.date.get.time.nanosecond
+  dt.date.get.time.snd.nanosecond
 
 /--
 Gets the `Weekday` of a DateTime.
@@ -449,14 +449,14 @@ def quarter (date : DateTime tz) : Bounded.LE 1 4 :=
 Getter for the `PlainTime` inside of a `DateTime`
 -/
 @[inline]
-def time (zdt : DateTime tz) : PlainTime :=
-  zdt.date.get.time
+def time (zdt : DateTime tz) : PlainTime zdt.date.get.time.fst :=
+  zdt.date.get.time.snd
 
 /--
 Converts a `DateTime` to the number of days since the UNIX epoch.
 -/
 @[inline]
-def ofDaysSinceUNIXEpoch (days : Day.Offset) (time : PlainTime) (tz : TimeZone) : DateTime tz :=
+def ofDaysSinceUNIXEpoch (days : Day.Offset) (time : PlainTime leap) (tz : TimeZone) : DateTime tz :=
   DateTime.ofPlainDateTime (PlainDateTime.ofDaysSinceUNIXEpoch days time) tz
 
 instance : HAdd (DateTime tz) (Day.Offset) (DateTime tz) where
diff --git a/src/Std/Time/Zoned/ZonedDateTime.lean b/src/Std/Time/Zoned/ZonedDateTime.lean
index b7b3d1f94382..fed4c5680a64 100644
--- a/src/Std/Time/Zoned/ZonedDateTime.lean
+++ b/src/Std/Time/Zoned/ZonedDateTime.lean
@@ -137,8 +137,8 @@ def toDateTime (dt : ZonedDateTime) : DateTime dt.timezone :=
 Getter for the `PlainTime` inside of a `ZonedDateTime`
 -/
 @[inline]
-def time (zdt : ZonedDateTime) : PlainTime :=
-  zdt.date.get.time
+def time (zdt : ZonedDateTime) : PlainTime zdt.date.get.time.fst :=
+  zdt.date.get.time.snd
 
 /--
 Getter for the `Year` inside of a `ZonedDateTime`
@@ -166,7 +166,7 @@ Getter for the `Hour` inside of a `ZonedDateTime`
 -/
 @[inline]
 def hour (zdt : ZonedDateTime) : Hour.Ordinal :=
-  zdt.date.get.time.hour
+  zdt.date.get.time.snd.hour
 
 /--
 Getter for the `Minute` inside of a `ZonedDateTime`
@@ -179,22 +179,22 @@ def minute (zdt : ZonedDateTime) : Minute.Ordinal :=
 Getter for the `Second` inside of a `ZonedDateTime`
 -/
 @[inline]
-def second (zdt : ZonedDateTime) : Second.Ordinal zdt.date.get.time.second.fst :=
-  zdt.date.get.time.second.snd
+def second (zdt : ZonedDateTime) : Second.Ordinal zdt.date.get.time.fst :=
+  zdt.date.get.time.snd.second
 
 /--
 Getter for the `Millisecond` inside of a `ZonedDateTime`.
 -/
 @[inline]
 def millisecond (dt : ZonedDateTime) : Millisecond.Ordinal :=
-  dt.date.get.time.millisecond
+  dt.date.get.time.snd.millisecond
 
 /--
 Getter for the `Nanosecond` inside of a `ZonedDateTime`
 -/
 @[inline]
 def nanosecond (zdt : ZonedDateTime) : Nanosecond.Ordinal :=
-  zdt.date.get.time.nanosecond
+  zdt.date.get.time.snd.nanosecond
 
 /--
 Getter for the `TimeZone.Offset` inside of a `ZonedDateTime`
@@ -493,7 +493,7 @@ Creates a new `ZonedDateTime` by adjusting the `second` component.
 @[inline]
 def withSeconds (dt : ZonedDateTime) (second : Sigma Second.Ordinal) : ZonedDateTime :=
   let date := dt.date.get
-  ZonedDateTime.ofPlainDateTime (date.withSeconds second) dt.rules
+  ZonedDateTime.ofPlainDateTime (date.withSeconds second.snd) dt.rules
 
 /--
 Creates a new `ZonedDateTime` by adjusting the `nano` component with a new `millis` that will set
@@ -528,7 +528,7 @@ def toDaysSinceUNIXEpoch (date : ZonedDateTime) : Day.Offset :=
 Converts a `ZonedDateTime` to the number of days since the UNIX epoch.
 -/
 @[inline]
-def ofDaysSinceUNIXEpoch (days : Day.Offset) (time : PlainTime) (zt : TimeZone.ZoneRules) : ZonedDateTime :=
+def ofDaysSinceUNIXEpoch (days : Day.Offset) (time : PlainTime leap) (zt : TimeZone.ZoneRules) : ZonedDateTime :=
   ZonedDateTime.ofPlainDateTime (PlainDateTime.ofDaysSinceUNIXEpoch days time) zt
 
 instance : HAdd ZonedDateTime Day.Offset ZonedDateTime where
diff --git a/tests/lean/run/timeAPI.lean b/tests/lean/run/timeAPI.lean
index 1509c573cf7d..7e311b489850 100644
--- a/tests/lean/run/timeAPI.lean
+++ b/tests/lean/run/timeAPI.lean
@@ -587,7 +587,7 @@ Std.Time.Weekday.friday
 2023-06-09
 2023-06-09
 19517
-1686268800000
+1686268800
 1970-01-02
 
 -/
@@ -667,7 +667,7 @@ Std.Time.Weekday.tuesday
 12
 3
 9938
-858650584000
+858650584
 1970-01-02T00:00:00.000000000
 
 -/
@@ -709,7 +709,7 @@ Std.Time.Weekday.tuesday
 
   println! plaindatetime.toDaysSinceUNIXEpoch
   println! plaindatetime.toTimestampAssumingUTC
-  println! PlainDateTime.ofDaysSinceUNIXEpoch 1 PlainTime.midnight
+  println! PlainDateTime.ofDaysSinceUNIXEpoch (leap := True) 1 PlainTime.midnight
 
 /--
 info: 2024-09-13T02:01:02.000000000-03:00
@@ -741,7 +741,7 @@ Std.Time.Weekday.thursday
 37
 2
 19978
-1726117262000
+1726117262
 1970-01-02T00:00:00.000000000Z
 
 -/
@@ -783,7 +783,7 @@ Std.Time.Weekday.thursday
 
   println! zoned.toDaysSinceUNIXEpoch
   println! zoned.toTimestamp
-  println! DateTime.ofDaysSinceUNIXEpoch 1 PlainTime.midnight .UTC
+  println! DateTime.ofDaysSinceUNIXEpoch (leap := True) 1 PlainTime.midnight .UTC
 
 /--
 info: 1997-03-19T02:03:04.000000000[America/Sao_Paulo]
@@ -816,7 +816,7 @@ Std.Time.Weekday.tuesday
 12
 3
 9938
-858661384000
+858661384
 
 -/
 #guard_msgs in
@@ -867,8 +867,8 @@ info: 2023-06-09T00:00:00.000000000
 #guard_msgs in
 #eval do
   println! PlainDateTime.ofPlainDate date("2023-06-09")
-  println! PlainDateTime.ofPlainTime time("12:32:43")
-  println! PlainDateTime.ofDaysSinceUNIXEpoch 23332 time("12:32:43")
+  println! PlainDateTime.ofPlainTime (leap := True) time("12:32:43")
+  println! PlainDateTime.ofDaysSinceUNIXEpoch (leap := True) 23332 time("12:32:43")
 
 /--
 info: 1970-01-02T00:00:00.000000000Z
@@ -880,7 +880,7 @@ info: 1970-01-02T00:00:00.000000000Z
 -/
 #guard_msgs in
 #eval do
-  println! DateTime.ofDaysSinceUNIXEpoch 1 PlainTime.midnight .UTC
+  println! DateTime.ofDaysSinceUNIXEpoch (leap := True) 1 PlainTime.midnight .UTC
   println! DateTime.ofPlainDate date("1997-03-18") .UTC
   println! DateTime.ofPlainDateTime datetime("1997-03-18T00:01:02") .UTC
   println! DateTime.ofPlainDateTimeAssumingUTC datetime("1997-03-18T00:01:02") .UTC
@@ -898,7 +898,7 @@ info: 1970-01-02T00:00:00.000000000[UTC]
 -/
 #guard_msgs in
 #eval do
-  println! ZonedDateTime.ofDaysSinceUNIXEpoch 1 PlainTime.midnight .UTC
+  println! ZonedDateTime.ofDaysSinceUNIXEpoch (leap := True) 1 PlainTime.midnight .UTC
   println! ZonedDateTime.ofPlainDate date("1997-03-18") .UTC
   println! ZonedDateTime.ofPlainDateWithZone date("1997-03-18") .UTC
   println! ZonedDateTime.ofPlainDateTime datetime("1997-03-18T00:01:02") .UTC
diff --git a/tests/lean/run/timeClassOperations.lean b/tests/lean/run/timeClassOperations.lean
index 39f1967df911..c2d738a434ee 100644
--- a/tests/lean/run/timeClassOperations.lean
+++ b/tests/lean/run/timeClassOperations.lean
@@ -65,7 +65,7 @@ info: datetime("2000-01-19T03:02:01.000000000")
 #guard_msgs in
 #eval datetime - (1 : Day.Offset)
 
-def time := time("13:02:01")
+def time : LeapTime := time("13:02:01")
 
 /--
 info: time("14:02:01.000000000")
diff --git a/tests/lean/run/timeFormats.lean b/tests/lean/run/timeFormats.lean
index 31be8b6faf55..930889fd3afe 100644
--- a/tests/lean/run/timeFormats.lean
+++ b/tests/lean/run/timeFormats.lean
@@ -20,8 +20,8 @@ def jpTZ : TimeZone := timezone("Asia/Tokyo +09:00")
 
 def date₁ := zoned("2014-06-16T03:03:03-03:00")
 
-def time₁ := time("14:11:01")
-def time₂ := time("03:11:01")
+def time₁ : LeapTime := time("14:11:01")
+def time₂ : LeapTime := time("03:11:01")
 
 /--
 info: "Monday, June 16, 2014 03:03:03 -0300"
@@ -178,9 +178,9 @@ info: "Monday, June 16, 2014 03:03:03 -0300"
 info: "14:11:01"
 -/
 #guard_msgs in
-#eval Time24Hour.formatBuilder time₁.hour time₁.minute time₁.second
+#eval Time24Hour.formatBuilder time₁.hour time₁.minute ⟨true, time₁.second⟩
 
-def l := Time12Hour.formatBuilder time₁.hour.toRelative time₁.minute time₁.second (if time₁.hour.val > 12 then HourMarker.pm else HourMarker.am)
+def l := Time12Hour.formatBuilder time₁.hour.toRelative time₁.minute ⟨true, time₁.second⟩ (if time₁.hour.val > 12 then HourMarker.pm else HourMarker.am)
 
 /--
 info: "02:11:01 PM"
@@ -191,7 +191,7 @@ info: "02:11:01 PM"
 info: "03:11:01 AM"
 -/
 #guard_msgs in
-#eval Time12Hour.formatBuilder time₂.hour.toRelative time₂.minute time₂.second (if time₂.hour.val > 12 then HourMarker.pm else HourMarker.am)
+#eval Time12Hour.formatBuilder time₂.hour.toRelative time₂.minute ⟨true, time₂.second⟩ (if time₂.hour.val > 12 then HourMarker.pm else HourMarker.am)
 
 /--
 info: "06/16/2014"
@@ -245,7 +245,7 @@ info: date("2002-07-14")
 info: time("14:13:12.000000000")
 -/
 #guard_msgs in
-#eval time("14:13:12")
+#eval (time("14:13:12") : LeapTime )
 
 /--
 info: zoned("2002-07-14T14:13:12.000000000Z")
@@ -275,9 +275,9 @@ info: "14-13-12"
 Format
 -/
 
-def time₄ := time("23:13:12.324354679")
+def time₄ := (time("23:13:12.324354679") : LeapTime )
 def date₄ := date("2002-07-14")
-def datetime₅ := PlainDateTime.mk (PlainDate.ofYearMonthDayClip (-2000) 3 4) (PlainTime.mk 12 23 ⟨false, 12⟩ 0)
+def datetime₅ := PlainDateTime.mk (PlainDate.ofYearMonthDayClip (-2000) 3 4) (Sigma.mk true <| PlainTime.mk 12 23 12 0)
 def datetime₄ := datetime("2002-07-14T23:13:12.324354679")
 def zoned₄ := zoned("2002-07-14T23:13:12.324354679+09:00")
 def zoned₅ := zoned("2002-07-14T23:13:12.324354679+00:00")
@@ -806,7 +806,7 @@ info: ("19343232432-01-04T01:04:03.000000000",
 -/
 #guard_msgs in
 #eval
-  let r := (PlainDateTime.mk (PlainDate.ofYearMonthDayClip 19343232432 1 4) (PlainTime.mk 25 64 ⟨true, 3⟩ 0))
+  let r := (PlainDateTime.mk (PlainDate.ofYearMonthDayClip 19343232432 1 4) (Sigma.mk true <| PlainTime.mk 25 64 3 0))
   let s := r.toLeanDateTimeString
   let r := PlainDateTime.parse s
   (s, r, datetime("1932-01-02T05:04:03.000000000"))
diff --git a/tests/lean/run/timeLocalDateTime.lean b/tests/lean/run/timeLocalDateTime.lean
index 4863a638729a..6da164c55639 100644
--- a/tests/lean/run/timeLocalDateTime.lean
+++ b/tests/lean/run/timeLocalDateTime.lean
@@ -5,7 +5,8 @@ open Std.Time
 def ShortDateTime : GenericFormat .any := datespec("dd/MM/uuuu HH:mm:ss")
 def ShortDate : GenericFormat .any := datespec("dd/MM/uuuu")
 
-def format (PlainDate : PlainDateTime) : String := ShortDateTime.formatBuilder PlainDate.day PlainDate.month PlainDate.year PlainDate.time.hour PlainDate.minute PlainDate.time.second
+def format (PlainDate : PlainDateTime) : String := ShortDateTime.formatBuilder PlainDate.day PlainDate.month PlainDate.year PlainDate.time.snd.hour PlainDate.minute ⟨PlainDate.time.fst, PlainDate.time.snd.second⟩
+
 def format₂ (PlainDate : PlainDate) : String := ShortDate.formatBuilder PlainDate.day PlainDate.month PlainDate.year
 
 def date₁ := datetime("1993-11-19T09:08:07")
diff --git a/tests/lean/run/timeOperations.lean b/tests/lean/run/timeOperations.lean
index 2aee656f9121..37fe808b8e95 100644
--- a/tests/lean/run/timeOperations.lean
+++ b/tests/lean/run/timeOperations.lean
@@ -131,7 +131,7 @@ info: datetime("1999-01-20T03:02:01.000000000")
 #guard_msgs in
 #eval datetime.subYearsRollOver 1
 
-def time := time("13:02:01")
+def time : LeapTime := time("13:02:01")
 
 /--
 info: time("14:02:01.000000000")
diff --git a/tests/lean/run/timeParse.lean b/tests/lean/run/timeParse.lean
index fcd7b6be0b77..72af186a45ed 100644
--- a/tests/lean/run/timeParse.lean
+++ b/tests/lean/run/timeParse.lean
@@ -21,8 +21,8 @@ def jpTZ : TimeZone := timezone("Asia/Tokyo +09:00")
 
 def date₁ := zoned("2014-06-16T03:03:03-03:00")
 
-def time₁ := time("14:11:01")
-def time₂ := time("03:11:01")
+def time₁ : LeapTime := time("14:11:01")
+def time₂ : LeapTime := time("03:11:01")
 
 /--
 info: "2014-06-16T03:03:03.000000100-03:00"
diff --git a/tests/lean/run/timeSet.lean b/tests/lean/run/timeSet.lean
index 4f179d506132..23b165273438 100644
--- a/tests/lean/run/timeSet.lean
+++ b/tests/lean/run/timeSet.lean
@@ -21,8 +21,8 @@ def jpTZ : TimeZone := timezone("Asia/Tokyo +09:00")
 
 def date₁ := zoned("2014-06-16T10:03:03-03:00")
 
-def time₁ := time("14:11:01")
-def time₂ := time("03:11:01")
+def time₁ : LeapTime := time("14:11:01")
+def time₂ : LeapTime := time("03:11:01")
 
 /--
 info: "2014-06-16T10:03:03.000000100-03:00"