From cac080f504cfee35808c9a1487990059ce43a21f Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 22 Apr 2019 13:42:53 -0700 Subject: [PATCH] test(tests/playground/mapVShmap): use `{x with ...}` notation in the test --- tests/playground/mapVShmap.lean | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/tests/playground/mapVShmap.lean b/tests/playground/mapVShmap.lean index 2a2b9ebd48..11e49d1c5c 100644 --- a/tests/playground/mapVShmap.lean +++ b/tests/playground/mapVShmap.lean @@ -9,13 +9,14 @@ set_option pp.binder_types false def f1 (ps : Array (Nat × Nat)) : Array (Nat × Nat) := ps.hmap (λ p, - -- let p := dbgTraceIfShared "bad1" p in - match p with (n, m) := (n+1, m)) + -- let p := dbgTraceIfShared "bad1" p in + { p with fst := p.fst + 1 }) def f2 (ps : Array (Nat × Nat)) : Array (Nat × Nat) := ps.map (λ p, -- let p := dbgTraceIfShared "bad2" p in - match p with (n, m) := (n+1, m)) + { p with fst := p.fst + 1 }) + def prof {α : Type} (msg : String) (p : IO α) : IO α := let msg₁ := "Time for '" ++ msg ++ "':" in