revert: change in plaindatetime derivings

leanprover · Jan 10, 2025 · 4870cb1 · 4870cb1
1 parent 572bae9
commit 4870cb1
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/src/Std/Time/DateTime/PlainDateTime.lean b/src/Std/Time/DateTime/PlainDateTime.lean
@@ -30,7 +30,8 @@ structure PlainDateTime where
   -/
   time : PlainTime
 
-  deriving Repr, Inhabited
+  deriving Inhabited, BEq, Repr
+
 
 namespace PlainDateTime