fix test

leanprover · Sep 23, 2024 · 3ef63b2 · 3ef63b2
1 parent 1769ea4
commit 3ef63b2
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/tests/lean/run/2670.lean b/tests/lean/run/2670.lean
@@ -12,12 +12,12 @@ def enumFromTR' (n : Nat) (l : List α) : List (Nat × α) :=
 
 open List in
 theorem enumFrom_eq_enumFromTR' : @enumFrom = @enumFromTR' := by
-  funext α n l; simp [enumFromTR', -Array.size_toArray]
+  funext α n l; simp only [enumFromTR']
   let f := fun (a : α) (n, acc) => (n-1, (n-1, a) :: acc)
   let rec go : ∀ l n, l.foldr f (n + l.length, []) = (n, enumFrom n l)
     | [], n => rfl
     | a::as, n => by
       rw [← show _ + as.length = n + (a::as).length from Nat.succ_add .., List.foldr, go as]
       simp [enumFrom, f]
-  rw [Array.foldr_eq_foldr_data]
+  rw [Array.foldr_eq_foldr_toList]
   simp [go] -- Should close the goal