From afc2569f7ce9d2f4b2269bef02a69cfd3b4c54bb Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 8 Feb 2019 11:00:48 -0800
Subject: [PATCH] fix(library/init/data/nat/basic): tail recursive nat.repeat

---
 library/init/data/nat/basic.lean | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/library/init/data/nat/basic.lean b/library/init/data/nat/basic.lean
index d7b0d66a68..7081b370a0 100644
--- a/library/init/data/nat/basic.lean
+++ b/library/init/data/nat/basic.lean
@@ -77,9 +77,12 @@ instance : has_sub nat :=
 instance : has_mul nat :=
 ⟨nat.mul⟩
 
-@[specialize] def {u} repeat {α : Type u} (f : nat → α → α) : nat → α → α
-| 0         m := m
-| (succ n)  m := f n (repeat n m)
+@[specialize] def {u} repeat_core {α : Type u} (f : nat → α → α) (s : nat) : nat → α → α
+| 0         a := a
+| (succ n)  a := repeat_core n (f (s - (succ n)) a)
+
+@[inline] def {u} repeat {α : Type u} (f : nat → α → α) (n : nat) (a : α) : α :=
+repeat_core f n n a
 
 protected def pow (m : nat) : nat → nat
 | 0        := 1