From 266808c570f7e9bbd62bf3928d745303307d4154 Mon Sep 17 00:00:00 2001
From: Adrian Palacios <accorell@amazon.com>
Date: Fri, 28 Feb 2025 17:40:57 -0500
Subject: [PATCH] Move instances to testing file, delete leftover theo

Signed-off-by: Adrian Palacios <accorell@amazon.com>
---
 cedar-lean/Cedar/Spec/Ext/Datetime.lean | 11 -----------
 cedar-lean/UnitTest/Datetime.lean       | 11 ++++++++++-
 2 files changed, 10 insertions(+), 12 deletions(-)

diff --git a/cedar-lean/Cedar/Spec/Ext/Datetime.lean b/cedar-lean/Cedar/Spec/Ext/Datetime.lean
index a65e9f8d8..4aacac2b8 100644
--- a/cedar-lean/Cedar/Spec/Ext/Datetime.lean
+++ b/cedar-lean/Cedar/Spec/Ext/Datetime.lean
@@ -136,17 +136,6 @@ instance Duration.decLe (d₁ d₂ : Duration) : Decidable (d₁ ≤ d₂) :=
 instance : Coe Int64 Duration where
   coe i := Duration.mk i
 
--- Note: The instances below are only used for tests.
--- We might redefine them if they are need for something else.
-instance : OfNat Duration n where
-  ofNat := ⟨Int64.ofNat n⟩
-
-instance : ToString Duration where
-  toString d := toString d.val
-
-instance : Neg Duration where
-  neg d := ⟨-d.val⟩
-
 def MILLISECONDS_PER_SECOND: Int := 1000
 def MILLISECONDS_PER_MINUTE: Int := 60000
 def MILLISECONDS_PER_HOUR: Int := 360000
diff --git a/cedar-lean/UnitTest/Datetime.lean b/cedar-lean/UnitTest/Datetime.lean
index 5ab8f3456..6cf5e07d9 100644
--- a/cedar-lean/UnitTest/Datetime.lean
+++ b/cedar-lean/UnitTest/Datetime.lean
@@ -89,7 +89,16 @@ def testsForInvalidDatetimeStrings :=
     testInvalidDatetime "2016-12-31T00:00:00+9999" "invalid offset range",
   ]
 
-theorem testDuration16 : toString ((Duration.parse "0d0h0m0s0ms").get!) = "0" := by native_decide
+-- Note: The instances below are only used for tests.
+-- We might redefine them if they are need for something else.
+instance : OfNat Duration n where
+  ofNat := ⟨Int64.ofNat n⟩
+
+instance : ToString Duration where
+  toString d := toString d.val
+
+instance : Neg Duration where
+  neg d := ⟨-d.val⟩
 
 private def testValidDuration (str : String) (rep : Int) : TestCase IO :=
   test str ⟨λ _ => checkEq (Duration.parse str) (duration? rep)⟩