chore(tests): fix tests

This commit is contained in:
Leonardo de Moura 2019-03-29 11:25:26 -07:00
parent c134617ee3
commit 4149a25186
4 changed files with 7 additions and 7 deletions

View file

@ -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)

View file

@ -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

View file

@ -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)) *>

View file

@ -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