From 8e0870beec487d55672525fbf1c66cdad93bf033 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Henrik=20B=C3=B6ving?= <hargonix@gmail.com>
Date: Tue, 20 May 2025 13:33:49 +0200
Subject: [PATCH] feat: LT for Timestamp and Duration (#8422)

This PR adds `LT` and `Decidable` `LT` instances for
`Std.Time.Timestamp` and `Std.Time.Duration`.
---
 src/Std/Time/DateTime/Timestamp.lean | 6 ++++++
 src/Std/Time/Duration.lean           | 6 ++++++
 2 files changed, 12 insertions(+)

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`
 -/