From 62b8954ec4dec6c73bea5e41f6ceedbeb2dcce36 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 19 Apr 2019 11:11:30 -0700 Subject: [PATCH] chore(library/init/data/array/basic): heterogeneous Array.mmap --- library/init/data/array/basic.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/library/init/data/array/basic.lean b/library/init/data/array/basic.lean index 4c369802e0..826e3eb579 100644 --- a/library/init/data/array/basic.lean +++ b/library/init/data/array/basic.lean @@ -196,8 +196,8 @@ miterate a ⟨a, rfl⟩ $ λ i v ⟨a', h⟩, do @[inline] def mforeach (a : Array α) (f : Π i : Fin a.size, α → m α) : m (Array α) := Subtype.val <$> mforeachAux a f -@[inline] def mmap (f : α → m α) (a : Array α) : m (Array α) := -mforeach a (λ _, f) +@[inline] def mmap {β : Type u} (f : α → m β) (as : Array α) : m (Array β) := +as.mfoldl (mkEmpty as.size) (λ a bs, do b ← f a, pure (bs.push b)) end @[inline] def foreach (a : Array α) (f : Π i : Fin a.size, α → α) : Array α :=