fix tests

leanprover · Sep 9, 2024 · 2a95bd7 · 2a95bd7
1 parent e740718
commit 2a95bd7
Show file tree

Hide file tree

Showing 6 changed files with 7 additions and 7 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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