diff --git a/tests/compiler/append.lean b/tests/compiler/append.lean index 508eadae60..5bb5f22ce4 100644 --- a/tests/compiler/append.lean +++ b/tests/compiler/append.lean @@ -1,4 +1,4 @@ def main (xs : List String) : IO Unit := -let ys1 := List.repeat 1 1000000 in -let ys2 := List.repeat 2 1000000 in +let ys1 := List.replicate 1000000 1 in +let ys2 := List.replicate 1000000 2 in IO.println (toString (ys1 ++ ys2).length) diff --git a/tests/compiler/map_big.lean b/tests/compiler/map_big.lean index 826cc981cf..4fc10b1645 100644 --- a/tests/compiler/map_big.lean +++ b/tests/compiler/map_big.lean @@ -1,8 +1,8 @@ def f2 (n : Nat) (xs : List Nat) : List (List Nat) := -let ys := List.repeat 0 n in +let ys := List.replicate n 0 in xs.map (λ x, x :: ys) def main : IO UInt32 := let n := 100000 in -IO.println (toString (f2 n (List.repeat 0 n)).length) *> +IO.println (toString (f2 n (List.replicate n 0)).length) *> pure 0 diff --git a/tests/compiler/thunk.lean b/tests/compiler/thunk.lean index 166c6887b3..600e28c94f 100644 --- a/tests/compiler/thunk.lean +++ b/tests/compiler/thunk.lean @@ -1,9 +1,9 @@ def compute (v : Nat) : Thunk Nat := -⟨λ _, let xs := List.repeat v 100000 in xs.foldl (+) 0⟩ +⟨λ _, let xs := List.replicate 100000 v in xs.foldl (+) 0⟩ @[noinline] def test (t : Thunk Nat) (n : Nat) : Nat := -n.repeat (λ i r, t.get + r) 0 +n.repeat (λ r, t.get + r) 0 def main (xs : List String) : IO UInt32 := IO.println (toString (test (compute 1) 100000)) *> diff --git a/tests/lean/run/array1.lean b/tests/lean/run/array1.lean index cc28be1be8..97995386d9 100644 --- a/tests/lean/run/array1.lean +++ b/tests/lean/run/array1.lean @@ -9,7 +9,7 @@ def f : Fin w.sz → Nat := Array.casesOn w (λ _ f, f) def arraySum (a : Array Nat) : Nat := -a.foldl 0 (+) +a.foldl (+) 0 #exit