From 4a3eccade72f99b9462fa426cc36f0291d547b80 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 28 Oct 2019 13:39:47 -0700 Subject: [PATCH] chore: fix name --- library/Init/Data/Nat/Control.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/Init/Data/Nat/Control.lean b/library/Init/Data/Nat/Control.lean index 334d285715..5bf22ab9bc 100644 --- a/library/Init/Data/Nat/Control.lean +++ b/library/Init/Data/Nat/Control.lean @@ -36,7 +36,7 @@ foldMAux f n n a | 0, a => pure a | i+1, a => f i a >>= foldRevMAux i -@[inline] def mfoldRev {α : Type u} {m : Type u → Type v} [Monad m] (f : Nat → α → m α) (a : α) (n : Nat) : m α := +@[inline] def foldRevM {α : Type u} {m : Type u → Type v} [Monad m] (f : Nat → α → m α) (a : α) (n : Nat) : m α := foldRevMAux f n a end Nat