From bcc49d1c5fc3d07652bd3edd660502521c97bf61 Mon Sep 17 00:00:00 2001
From: Scott Morrison <scott.morrison@gmail.com>
Date: Fri, 22 Dec 2023 09:22:47 +1100
Subject: [PATCH] chore: update tests for #2966 to use test_extern (#3092)

#2966 was the `@[extern]` bug that prompted development of the
`test_extern` command, but then we merged the fix to #2966 without
updating the tests to use `test_extern`.
---
 tests/lean/run/2966.lean | 96 ++++++++++------------------------------
 1 file changed, 23 insertions(+), 73 deletions(-)

diff --git a/tests/lean/run/2966.lean b/tests/lean/run/2966.lean
index 88dfd1797c04..4312c5a0d113 100644
--- a/tests/lean/run/2966.lean
+++ b/tests/lean/run/2966.lean
@@ -1,81 +1,31 @@
-import Lean
+import Lean.Util.TestExtern
 
-def testCopySlice (src : Array UInt8) (srcOff : Nat) (dest : Array UInt8) (destOff len : Nat) : Bool :=
-  (ByteArray.copySlice ⟨src⟩ srcOff ⟨dest⟩ destOff len |>.toList) ==
-    (ByteArray.copySlice ⟨src⟩ srcOff ⟨dest⟩ destOff len |>.toList)
-
--- We verify that the `@[extern]` implementation of `ByteArray.copySlice` matches the formal definition,
--- by equating two copies using `==`, unfolding the definition of one, and then calling `native_decide`
-macro "testCopySliceTactic" : tactic =>
-  `(tactic|
-      (dsimp [testCopySlice]
-       conv =>
-        congr
-        congr
-        dsimp [ByteArray.copySlice]
-       native_decide))
+deriving instance DecidableEq for ByteArray
 
 -- These used to fail, as reported in #2966
+test_extern ByteArray.copySlice ⟨#[1,2,3]⟩ 1 ⟨#[4, 5, 6, 7, 8, 9, 10, 11, 12, 13]⟩ 0 6
 
-example : testCopySlice #[1,2,3] 1 #[4, 5, 6, 7, 8, 9, 10, 11, 12, 13] 0 6 := by
-  testCopySliceTactic
-
-example : testCopySlice #[1,2,3] 1 #[4, 5, 6, 7, 8, 9, 10, 11, 12, 13] 0 20 := by
-  testCopySliceTactic
-
-example : testCopySlice #[1,2,3] 1 #[4, 5, 6] 0 6 := by
-  testCopySliceTactic
-
-example : testCopySlice #[1,2,3] 1 #[4, 5, 6, 7, 8, 9, 10, 11, 12, 13] 1 6 := by
-  testCopySliceTactic
-
-example : testCopySlice #[1,2,3] 1 #[4, 5, 6, 7, 8, 9, 10, 11, 12, 13] 1 20 := by
-  testCopySliceTactic
-
-example : testCopySlice #[1,2,3] 0 #[4, 5, 6, 7, 8, 9, 10, 11, 12, 13] 0 6 := by
-  testCopySliceTactic
-
-example : testCopySlice #[1,2,3] 0 #[4, 5, 6, 7, 8, 9, 10, 11, 12, 13] 0 20 := by
-  testCopySliceTactic
-
-example : testCopySlice #[1,2,3] 0 #[4, 5, 6, 7, 8, 9, 10, 11, 12, 13] 1 6 := by
-  testCopySliceTactic
-
-example : testCopySlice #[1,2,3] 0 #[4, 5, 6, 7, 8, 9, 10, 11, 12, 13] 1 20 := by
-  testCopySliceTactic
+test_extern ByteArray.copySlice ⟨#[1,2,3]⟩ 1 ⟨#[4, 5, 6, 7, 8, 9, 10, 11, 12, 13]⟩ 0 6
+test_extern ByteArray.copySlice ⟨#[1,2,3]⟩ 1 ⟨#[4, 5, 6, 7, 8, 9, 10, 11, 12, 13]⟩ 0 20
 
+test_extern ByteArray.copySlice ⟨#[1,2,3]⟩ 1 ⟨#[4, 5, 6]⟩ 0 6
+test_extern ByteArray.copySlice ⟨#[1,2,3]⟩ 1 ⟨#[4, 5, 6, 7, 8, 9, 10, 11, 12, 13]⟩ 1 6
+test_extern ByteArray.copySlice ⟨#[1,2,3]⟩ 1 ⟨#[4, 5, 6, 7, 8, 9, 10, 11, 12, 13]⟩ 1 20
+test_extern ByteArray.copySlice ⟨#[1,2,3]⟩ 0 ⟨#[4, 5, 6, 7, 8, 9, 10, 11, 12, 13]⟩ 0 6
+test_extern ByteArray.copySlice ⟨#[1,2,3]⟩ 0 ⟨#[4, 5, 6, 7, 8, 9, 10, 11, 12, 13]⟩ 0 20
+test_extern ByteArray.copySlice ⟨#[1,2,3]⟩ 0 ⟨#[4, 5, 6, 7, 8, 9, 10, 11, 12, 13]⟩ 1 6
+test_extern ByteArray.copySlice ⟨#[1,2,3]⟩ 0 ⟨#[4, 5, 6, 7, 8, 9, 10, 11, 12, 13]⟩ 1 20
 
 -- These worked prior to #2966; extra text cases can't hurt!
 
-example : testCopySlice #[1,2,3] 1 #[4, 5, 6, 7, 8, 9, 10, 11, 12, 13] 0 2 := by
-  testCopySliceTactic
-
-example : testCopySlice #[1,2,3] 1 #[4, 5, 6] 0 2 := by
-  testCopySliceTactic
-
-example : testCopySlice #[1,2,3] 1 #[4, 5, 6, 7, 8, 9, 10, 11, 12, 13] 1 2 := by
-  testCopySliceTactic
-
-example : testCopySlice #[1,2,3] 1 #[4, 5, 6] 1 2 := by
-  testCopySliceTactic
-
-example : testCopySlice #[1,2,3] 1 #[4, 5, 6] 1 6 := by
-  testCopySliceTactic
-
-example : testCopySlice #[1,2,3] 1 #[4, 5, 6, 7, 8, 9, 10, 11, 12, 13] 0 2 := by
-  testCopySliceTactic
-
-example : testCopySlice #[1,2,3] 0 #[4, 5, 6] 0 2 := by
-  testCopySliceTactic
-
-example : testCopySlice #[1,2,3] 0 #[4, 5, 6, 7, 8, 9, 10, 11, 12, 13] 1 2 := by
-  testCopySliceTactic
-
-example : testCopySlice #[1,2,3] 0 #[4, 5, 6] 1 2 := by
-  testCopySliceTactic
-
-example : testCopySlice #[1,2,3] 0 #[4, 5, 6] 1 6 := by
-  testCopySliceTactic
-
-example : testCopySlice #[1,2,3] 0 #[4, 5, 6] 0 6 := by
-  testCopySliceTactic
+test_extern ByteArray.copySlice ⟨#[1,2,3]⟩ 1 ⟨#[4, 5, 6, 7, 8, 9, 10, 11, 12, 13]⟩ 0 2
+test_extern ByteArray.copySlice ⟨#[1,2,3]⟩ 1 ⟨#[4, 5, 6]⟩ 0 2
+test_extern ByteArray.copySlice ⟨#[1,2,3]⟩ 1 ⟨#[4, 5, 6, 7, 8, 9, 10, 11, 12, 13]⟩ 1 2
+test_extern ByteArray.copySlice ⟨#[1,2,3]⟩ 1 ⟨#[4, 5, 6]⟩ 1 2
+test_extern ByteArray.copySlice ⟨#[1,2,3]⟩ 1 ⟨#[4, 5, 6]⟩ 1 6
+test_extern ByteArray.copySlice ⟨#[1,2,3]⟩ 1 ⟨#[4, 5, 6, 7, 8, 9, 10, 11, 12, 13]⟩ 0 2
+test_extern ByteArray.copySlice ⟨#[1,2,3]⟩ 0 ⟨#[4, 5, 6]⟩ 0 2
+test_extern ByteArray.copySlice ⟨#[1,2,3]⟩ 0 ⟨#[4, 5, 6, 7, 8, 9, 10, 11, 12, 13]⟩ 1 2
+test_extern ByteArray.copySlice ⟨#[1,2,3]⟩ 0 ⟨#[4, 5, 6]⟩ 1 2
+test_extern ByteArray.copySlice ⟨#[1,2,3]⟩ 0 ⟨#[4, 5, 6]⟩ 1 6
+test_extern ByteArray.copySlice ⟨#[1,2,3]⟩ 0 ⟨#[4, 5, 6]⟩ 0 6