max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

test(tests/playground/mapVShmap): use {x with ...} notation in the test

Browse source
This commit is contained in:
Leonardo de Moura 2019-04-22 13:42:53 -07:00
parent f222dc7cca
commit cac080f504
1 changed files with 4 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
tests/playground/mapVShmap.lean
View file

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