From ff47eba9d1ef2ca39768890ab20c70207386f2dc Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 9 May 2019 07:43:13 -0700 Subject: [PATCH] fix(library/init/control/combinators): iterate forward --- library/init/control/combinators.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/library/init/control/combinators.lean b/library/init/control/combinators.lean index 7619b3224a..4dad03a1e5 100644 --- a/library/init/control/combinators.lean +++ b/library/init/control/combinators.lean @@ -32,12 +32,12 @@ mcond c t (pure ()) namespace Nat -@[specialize] def mforAux {m} [Applicative m] (f : Nat → m Unit) : Nat → m Unit +@[specialize] def mforAux {m} [Applicative m] (f : Nat → m Unit) (n : Nat) : Nat → m Unit | 0 := pure () -| (i+1) := f i *> mforAux i +| (i+1) := f (n-i-1) *> mforAux i @[inline] def mfor {m} [Applicative m] (n : Nat) (f : Nat → m Unit) : m Unit := -mforAux f n +mforAux f n n -- TODO: enable after we have support for marking arguments that should be considered for specialization. /-