diff --git a/tests/playground/task_test.lean b/tests/playground/task_test.lean index 383091ad5d..636ce43bc3 100644 --- a/tests/playground/task_test.lean +++ b/tests/playground/task_test.lean @@ -13,8 +13,8 @@ dbgTrace ("f2: " ++ toString x) $ fun _ => g x def main (xs : List String) : IO UInt32 := -let t1 := Task.mk $ (fun _ => f1 xs.head.toNat) in -let t2 := Task.mk $ (fun _ => f2 xs.head.toNat) in +let t1 := Task.mk $ (fun _ => f1 xs.head.toNat); +let t2 := Task.mk $ (fun _ => f2 xs.head.toNat); dbgSleep 1000 $ fun _ => IO.println (toString t1.get ++ " " ++ toString t2.get) *> pure 0 diff --git a/tests/playground/task_test2.lean b/tests/playground/task_test2.lean index d5e26e1ae5..3d0a8aa9ca 100644 --- a/tests/playground/task_test2.lean +++ b/tests/playground/task_test2.lean @@ -5,8 +5,8 @@ n.repeat (fun r => 0 def main (xs : List String) : IO UInt32 := -let ys := (List.replicate xs.head.toNat 1) in -let ts : List (Task Nat) := (List.iota 10).map (fun i => Task.mk $ fun _ => run1 (i+1) xs.head.toNat ys) in -let ns : List Nat := ts.map Task.get in +let ys := (List.replicate xs.head.toNat 1); +let ts : List (Task Nat) := (List.iota 10).map (fun i => Task.mk $ fun _ => run1 (i+1) xs.head.toNat ys); +let ns : List Nat := ts.map Task.get; IO.println (">> " ++ toString ns) *> pure 0 diff --git a/tests/playground/task_test3.lean b/tests/playground/task_test3.lean index a3efb5ccc0..b23d687573 100644 --- a/tests/playground/task_test3.lean +++ b/tests/playground/task_test3.lean @@ -5,8 +5,8 @@ n.repeat (fun r => 0 def main (xs : List String) : IO UInt32 := -let ys := (List.replicate xs.head.toNat 1) in -let ts : List (Task Nat) := (List.iota 10).map (fun i => Task.mk $ fun _ => run1 (i+1) xs.head.toNat ys) in -let ns : List Nat := ts.map Task.get in +let ys := (List.replicate xs.head.toNat 1); +let ts : List (Task Nat) := (List.iota 10).map (fun i => Task.mk $ fun _ => run1 (i+1) xs.head.toNat ys); +let ns : List Nat := ts.map Task.get; IO.println (">> " ++ toString ns) *> pure 0 diff --git a/tests/playground/task_test4.lean b/tests/playground/task_test4.lean index 46b53a7db7..1c95e5a60c 100644 --- a/tests/playground/task_test4.lean +++ b/tests/playground/task_test4.lean @@ -1,12 +1,12 @@ def run1 (i : Nat) (n : Nat) (xs : List Nat) : Nat := n.repeat (fun r => - let s := (">> [" ++ toString i ++ "] " ++ toString r) in + let s := (">> [" ++ toString i ++ "] " ++ toString r); xs.foldl (fun a b => a + b) (r + s.length)) 0 def main (xs : List String) : IO UInt32 := -let ys := (List.replicate xs.head.toNat 1) in -let ts : List (Task Nat) := (List.iota 10).map (fun i => Task.mk $ fun _ => run1 (i+1) xs.head.toNat ys) in -let ns : List Nat := ts.map Task.get in +let ys := (List.replicate xs.head.toNat 1); +let ts : List (Task Nat) := (List.iota 10).map (fun i => Task.mk $ fun _ => run1 (i+1) xs.head.toNat ys); +let ns : List Nat := ts.map Task.get; IO.println (">> " ++ toString ns) *> pure 0