diff --git a/src/Std/Time/DateTime/Timestamp.lean b/src/Std/Time/DateTime/Timestamp.lean index b4976450f5..305a9b0d5c 100644 --- a/src/Std/Time/DateTime/Timestamp.lean +++ b/src/Std/Time/DateTime/Timestamp.lean @@ -34,6 +34,12 @@ instance : LE Timestamp where instance { x y : Timestamp } : Decidable (x ≤ y) := inferInstanceAs (Decidable (x.val ≤ y.val)) +instance : LT Timestamp where + lt x y := x.val < y.val + +instance { x y : Timestamp } : Decidable (x < y) := + inferInstanceAs (Decidable (x.val < y.val)) + instance : OfNat Timestamp n where ofNat := ⟨OfNat.ofNat n⟩ diff --git a/src/Std/Time/Duration.lean b/src/Std/Time/Duration.lean index d5ddb5b42a..e64318b413 100644 --- a/src/Std/Time/Duration.lean +++ b/src/Std/Time/Duration.lean @@ -156,6 +156,12 @@ instance : LE Duration where instance {x y : Duration} : Decidable (x ≤ y) := inferInstanceAs (Decidable (x.toNanoseconds ≤ y.toNanoseconds)) +instance : LT Duration where + lt d1 d2 := d1.toNanoseconds < d2.toNanoseconds + +instance {x y : Duration} : Decidable (x < y) := + inferInstanceAs (Decidable (x.toNanoseconds < y.toNanoseconds)) + /-- Converts a `Duration` to a `Minute.Offset` -/