From 2a95bd7d1670f3c954eb0e43bde7df22849f8c94 Mon Sep 17 00:00:00 2001
From: Kim Morrison <kim@tqft.net>
Date: Mon, 9 Sep 2024 21:26:51 +1000
Subject: [PATCH] fix tests

---
 src/Init/Data/Array/Basic.lean       | 2 +-
 src/library/constants.txt            | 2 +-
 tests/bench/liasolver.lean           | 2 +-
 tests/compiler/array.lean            | 2 +-
 tests/lean/run/PPTopDownAnalyze.lean | 4 ++--
 tests/lean/run/structInstFast.lean   | 2 +-
 6 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean
index 11a1d2c07c9f..4dd64eaefafc 100644
--- a/src/Init/Data/Array/Basic.lean
+++ b/src/Init/Data/Array/Basic.lean
@@ -497,7 +497,7 @@ def elem [BEq α] (a : α) (as : Array α) : Bool :=
       (true, r)
 
 /-- Convert a `Array α` into an `List α`. This is O(n) in the size of the array.  -/
--- This function is exported to C, where it is called by `Array.data`
+-- This function is exported to C, where it is called by `Array.toList`
 -- (the projection) to implement this functionality.
 @[export lean_array_to_list]
 def toListImpl (as : Array α) : List α :=
diff --git a/src/library/constants.txt b/src/library/constants.txt
index 481a20aa57cc..973c231dab49 100644
--- a/src/library/constants.txt
+++ b/src/library/constants.txt
@@ -7,7 +7,7 @@ And.rec
 And.casesOn
 Array
 Array.sz
-Array.data
+Array.toList
 autoParam
 bit0
 bit1
diff --git a/tests/bench/liasolver.lean b/tests/bench/liasolver.lean
index afd1cae2442e..8a5633b8e2ac 100644
--- a/tests/bench/liasolver.lean
+++ b/tests/bench/liasolver.lean
@@ -392,5 +392,5 @@ def main (args : List String) : IO UInt32 := do
       IO.println "UNSAT"
     | Solution.sat assignment =>
       IO.println "SAT"
-      IO.println <| String.intercalate " " <| assignment.data.map toString
+      IO.println <| String.intercalate " " <| assignment.toList.map toString
   return 0
diff --git a/tests/compiler/array.lean b/tests/compiler/array.lean
index d0bfc5e0a8ca..75d80cedd695 100644
--- a/tests/compiler/array.lean
+++ b/tests/compiler/array.lean
@@ -2,7 +2,7 @@
   Array.casesOn (motive := fun _ => Nat) a (fun data => data.length)
 
 @[noinline] def g (a : Array Nat) : List Nat :=
-  a.data
+  a.toList
 
 @[noinline] def h (a : List Nat) : List Nat :=
   g (Array.mk a)
diff --git a/tests/lean/run/PPTopDownAnalyze.lean b/tests/lean/run/PPTopDownAnalyze.lean
index 42e166ca0868..1a93555361ee 100644
--- a/tests/lean/run/PPTopDownAnalyze.lean
+++ b/tests/lean/run/PPTopDownAnalyze.lean
@@ -275,8 +275,8 @@ set_option pp.proofs.withType false in
 
 end proofs
 
-#testDelab ∀ (α : Type u) (vals vals_1 : List α), { data := vals : Array α } = { data := vals_1 : Array α }
-  expecting ∀ (α : Type u) (vals vals_1 : List α), { data := vals : Array α } = { data := vals_1 }
+#testDelab ∀ (α : Type u) (vals vals_1 : List α), { toList := vals : Array α } = { toList := vals_1 : Array α }
+  expecting ∀ (α : Type u) (vals vals_1 : List α), { toList := vals : Array α } = { toList := vals_1 }
 
 #testDelab (do let ctxCore ← readThe Core.Context; pure ctxCore.currNamespace : MetaM Name)
   expecting do
diff --git a/tests/lean/run/structInstFast.lean b/tests/lean/run/structInstFast.lean
index ecc40bc43f99..6992ebf549e5 100644
--- a/tests/lean/run/structInstFast.lean
+++ b/tests/lean/run/structInstFast.lean
@@ -63,7 +63,7 @@ where go (val : TSyntax `ident) (width depth : Nat) (cmds : Array <| TSyntax `co
     let cmd : TSyntax `command := ⟨mkNullNode cmds⟩
     `($cmd:command)
   | m+1 =>
-    let len := cmds.data.length
+    let len := cmds.toList.length
     let newTerm (s : String) := if len = 1 then baseTypeIdent else mkIdent' s (m+1)
     let newTerm' (s : String) := if len = 1 then baseIdent else mkIdent' s (m+1)
     let fieldsStx ← mkFieldsStx type (s!"x{m}_") width