diff --git a/tests/playground/task_test.lean b/tests/playground/task_test.lean index 06b85d2457..383091ad5d 100644 --- a/tests/playground/task_test.lean +++ b/tests/playground/task_test.lean @@ -1,20 +1,20 @@ def g (x : Nat) : Nat := -dbgTrace ("g: " ++ toString x) $ λ _, +dbgTrace ("g: " ++ toString x) $ fun _ => x + 1 def f1 (x : Nat) : Nat := -dbgSleep 1000 $ λ _, -dbgTrace ("f1: " ++ toString x) $ λ _, +dbgSleep 1000 $ fun _ => +dbgTrace ("f1: " ++ toString x) $ fun _ => g (x + 1) def f2 (x : Nat) : Nat := -dbgSleep 100 $ λ _, -dbgTrace ("f2: " ++ toString x) $ λ _, +dbgSleep 100 $ fun _ => +dbgTrace ("f2: " ++ toString x) $ fun _ => g x def main (xs : List String) : IO UInt32 := -let t1 := Task.mk $ (λ _, f1 xs.head.toNat) in -let t2 := Task.mk $ (λ _, f2 xs.head.toNat) in -dbgSleep 1000 $ λ _, +let t1 := Task.mk $ (fun _ => f1 xs.head.toNat) in +let t2 := Task.mk $ (fun _ => f2 xs.head.toNat) in +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 a97e1bca7c..d5e26e1ae5 100644 --- a/tests/playground/task_test2.lean +++ b/tests/playground/task_test2.lean @@ -1,12 +1,12 @@ def run1 (i : Nat) (n : Nat) (xs : List Nat) : Nat := -n.repeat (λ r, - dbgTrace (">> [" ++ toString i ++ "] " ++ toString r) $ λ _, - xs.foldl (+) r) +n.repeat (fun r => + dbgTrace (">> [" ++ toString i ++ "] " ++ toString r) $ fun _ => + xs.foldl (fun a b => a + b) 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 (λ i, Task.mk $ λ _, run1 (i+1) xs.head.toNat ys) 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 IO.println (">> " ++ toString ns) *> pure 0 diff --git a/tests/playground/task_test3.lean b/tests/playground/task_test3.lean index 8eb5b23a79..a3efb5ccc0 100644 --- a/tests/playground/task_test3.lean +++ b/tests/playground/task_test3.lean @@ -1,12 +1,12 @@ def run1 (i : Nat) (n : Nat) (xs : List Nat) : Nat := -n.repeat (λ r, +n.repeat (fun r => -- dbgTrace (">> [" ++ toString i ++ "] " ++ toString r) $ λ _, - xs.foldl (+) (r+i)) + xs.foldl (fun a b => a + b) (r+i)) 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 (λ i, Task.mk $ λ _, run1 (i+1) xs.head.toNat ys) 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 IO.println (">> " ++ toString ns) *> pure 0 diff --git a/tests/playground/task_test4.lean b/tests/playground/task_test4.lean index 3edc298630..46b53a7db7 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 (λ r, +n.repeat (fun r => let s := (">> [" ++ toString i ++ "] " ++ toString r) in - xs.foldl (+) (r + s.length)) + 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 (λ i, Task.mk $ λ _, run1 (i+1) xs.head.toNat ys) 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 IO.println (">> " ++ toString ns) *> pure 0