From fe9908cad33d5f8cf6adfa7779fb276ff7b4f159 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 31 Jul 2019 16:02:21 -0700
Subject: [PATCH] chore(tests/playground/persistentarray): fix test

---
 tests/playground/persistentarray.lean | 22 +++++++++++-----------
 1 file changed, 11 insertions(+), 11 deletions(-)

diff --git a/tests/playground/persistentarray.lean b/tests/playground/persistentarray.lean
index be7457fd11..d942964392 100644
--- a/tests/playground/persistentarray.lean
+++ b/tests/playground/persistentarray.lean
@@ -4,25 +4,25 @@ abbrev MyArray := PersistentArray Nat
 -- abbrev MyArray := Array Nat
 
 def mkMyArray (n : Nat) : MyArray :=
-n.fold (λ i s, s.push i) { PersistentArray . }
+n.fold (λ i s => s.push i) { PersistentArray . }
 -- n.fold (λ i s, s.push i) Array.empty
 
 def check (n : Nat) (p : Nat → Nat → Bool) (s : MyArray) : IO Unit :=
-n.mfor $ λ i, unless (p i (s.get i)) (throw (IO.userError ("failed at " ++ toString i ++ " " ++ toString (s.get i))))
+n.mfor $ λ i => unless (p i (s.get i)) (throw (IO.userError ("failed at " ++ toString i ++ " " ++ toString (s.get i))))
 
 def inc1 (n : Nat) (s : MyArray) : MyArray :=
-n.fold (λ i s, s.set i (s.get i + 1)) s
+n.fold (λ i s => s.set i (s.get i + 1)) s
 
 def checkId (n : Nat) (s : MyArray) : IO Unit :=
-check n (==) s
+check n (fun a b => a == b) s
 
 def main (xs : List String) : IO Unit :=
 do
-let n := xs.head.toNat,
-let t := mkMyArray n,
-checkId n t,
-let t := inc1 n t,
-check n (λ i v, v == i + 1) t,
-IO.println t.size,
-IO.println t.stats,
+let n := xs.head.toNat;
+let t := mkMyArray n;
+checkId n t;
+let t := inc1 n t;
+check n (λ i v => v == i + 1) t;
+IO.println t.size;
+IO.println t.stats;
 pure ()