From 49551036ed0bd96ebf96186d8282cdf2867fdbda Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 29 Mar 2019 10:39:00 -0700
Subject: [PATCH] refactor(library/init): minor changes
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Old `Nat.repeat` => `Nat.for`
Old `Nat.mrepeat` => `Nat.mfor`
New `Nat.repeat` has type
```
def repeat {α : Type u} (f : α → α) (n : Nat) (a : α) : α :=
``
`List.repeat` => `List.replicate` (like in Haskell)
Avoid weird `ℕ` in List library
---
 library/init/control/combinators.lean |  9 ++++--
 library/init/data/array/basic.lean    | 44 ++++++++++-----------------
 library/init/data/list/basic.lean     | 14 ++++-----
 library/init/data/nat/basic.lean      | 15 ++++++---
 library/init/data/string/basic.lean   |  2 +-
 5 files changed, 42 insertions(+), 42 deletions(-)

diff --git a/library/init/control/combinators.lean b/library/init/control/combinators.lean
index 9f58256956..29370e3c2f 100644
--- a/library/init/control/combinators.lean
+++ b/library/init/control/combinators.lean
@@ -31,8 +31,13 @@ mcond c t (pure ())
 namespace Nat
 
 @[specialize]
-def mrepeat {m} [Monad m] (n : Nat) (f : Nat → m Unit) : m Unit :=
-n.repeat (λ i a, a *> f i) (pure ())
+def mfor {m} [Monad m] (n : Nat) (f : Nat → m Unit) : m Unit :=
+n.for (λ i a, a *> f i) (pure ())
+
+@[specialize]
+def mrepeat {m} [Monad m] : Nat → m Unit → m Unit
+| 0     f := pure ()
+| (k+1) f := f *> mrepeat k f
 
 end Nat
 
diff --git a/library/init/data/array/basic.lean b/library/init/data/array/basic.lean
index c6fb5ab2e0..0010203c9e 100644
--- a/library/init/data/array/basic.lean
+++ b/library/init/data/array/basic.lean
@@ -42,7 +42,7 @@ def push (a : Array α) (v : α) : Array α :=
 
 def mkArray {α : Type u} (n : Nat) (v : α) : Array α :=
 let a : Array α := mkEmpty n in
-n.repeat (λ _ a, a.push v) a
+n.repeat (λ a, a.push v) a
 
 def empty : Array α :=
 mkEmpty 0
@@ -183,36 +183,24 @@ end Array
 
 export Array (mkArray)
 
-private theorem repeatCoreIndexIndep {α : Type u} (f : α → α) (n m₁ m₂ : Nat) :
-  ∀ (a : α), Nat.repeatCore (λ _ a, f a) m₁ n a =
-  Nat.repeatCore (λ _ a, f a) m₂ n a :=
-Nat.recOn n (λ a, rfl) (λ n ih a,
-  show Nat.repeatCore (λ _ a, f a) m₁ n (f a) =
-       Nat.repeatCore (λ _ a, f a) m₂ n (f a), from
-  ih (f a))
-
-private theorem repeatCorePushSz {α : Type u} : ∀ (n m : Nat) (v : α) (a : Array α),
-   (Nat.repeatCore (λ _ (a : Array α), a.push v) m n (a.push v)).sz =
-   (Nat.repeatCore (λ _ (a : Array α), a.push v) m n a).sz.succ
-| 0            _ _ _ := rfl
-| (Nat.succ n) m v a :=
-  show (Nat.repeatCore (λ _ (a : Array α), a.push v) m n ((a.push v).push v)).sz =
-       (Nat.repeatCore (λ _ (a : Array α), a.push v) m n (a.push v)).sz.succ, from
-  repeatCorePushSz n m v (a.push v)
+private theorem repeatCorePushSz {α : Type u} : ∀ (n : Nat) (v : α) (a : Array α),
+   (Nat.repeatCore (λ (a : Array α), a.push v) n (a.push v)).sz =
+   (Nat.repeatCore (λ (a : Array α), a.push v) n a).sz.succ
+| 0            _ _ := rfl
+| (Nat.succ n) v a :=
+  show (Nat.repeatCore (λ (a : Array α), a.push v) n ((a.push v).push v)).sz =
+       (Nat.repeatCore (λ (a : Array α), a.push v) n (a.push v)).sz.succ, from
+  repeatCorePushSz n v (a.push v)
 
 theorem szMkArrayEq {α : Type u} (n : Nat) (v : α) : (mkArray n v).sz = n :=
 Nat.recOn n rfl $ λ n ih,
-  have aux₁ : (Nat.repeatCore (λ _ (a : Array α), a.push v) n n (Array.mkEmpty n)).sz = n, from ih,
-  have aux₂ : (Nat.repeatCore (λ _ (a : Array α), a.push v) n.succ n (Array.mkEmpty n)).sz = n, from
-    repeatCoreIndexIndep (λ (a : Array α), a.push v) n n n.succ (Array.mkEmpty n) ▸ aux₁,
-  have aux₃ : (Nat.repeatCore (λ _ (a : Array α), a.push v) n.succ n ((Array.mkEmpty n).push v)).sz =
-              (Nat.repeatCore (λ _ (a : Array α), a.push v) n.succ n (Array.mkEmpty n)).sz.succ, from
-    repeatCorePushSz _ _ _ _,
-  have aux₄ : (Nat.repeatCore (λ _ (a : Array α), a.push v) n.succ n (Array.mkEmpty n)).sz.succ = n.succ, from
-    congrArg _ aux₂,
-  have aux₄ : (Nat.repeatCore (λ _ (a : Array α), a.push v) n.succ n ((Array.mkEmpty n).push v)).sz = n.succ, from
-    Eq.trans aux₃ aux₄,
-  aux₄
+  have aux₁ : (Nat.repeatCore (λ (a : Array α), a.push v) n (Array.mkEmpty n)).sz = n, from ih,
+  have aux₂ : (Nat.repeatCore (λ (a : Array α), a.push v) n ((Array.mkEmpty n).push v)).sz =
+              (Nat.repeatCore (λ (a : Array α), a.push v) n (Array.mkEmpty n)).sz.succ, from
+    repeatCorePushSz _ _ _,
+  have aux₃ : (Nat.repeatCore (λ (a : Array α), a.push v) n (Array.mkEmpty n)).sz.succ = n.succ, from
+    congrArg _ aux₁,
+  Eq.trans aux₂ aux₃
 
 @[inlineIfReduce] def List.toArrayAux {α : Type u} : List α → Array α → Array α
 | []      r := r
diff --git a/library/init/data/list/basic.lean b/library/init/data/list/basic.lean
index d5ca44cef2..3b51dc1e22 100644
--- a/library/init/data/list/basic.lean
+++ b/library/init/data/list/basic.lean
@@ -279,25 +279,25 @@ filter (∈ l₂) l₁
 instance [DecidableEq α] : HasInter (List α) :=
 ⟨List.inter⟩
 
-def repeat (a : α) (n : ℕ) : List α :=
-n.repeat (λ _ xs, a :: xs) []
+def replicate (n : Nat) (a : α) : List α :=
+n.repeat (λ xs, a :: xs) []
 
-def rangeCore : ℕ → List ℕ → List ℕ
+def rangeCore : Nat → List Nat → List Nat
 | 0        l := l
 | (succ n) l := rangeCore n (n :: l)
 
-def range (n : ℕ) : List ℕ :=
+def range (n : Nat) : List Nat :=
 rangeCore n []
 
-def iota : ℕ → List ℕ
+def iota : Nat → List Nat
 | 0        := []
 | (succ n) := succ n :: iota n
 
-def enumFrom : ℕ → List α → List (ℕ × α)
+def enumFrom : Nat → List α → List (Nat × α)
 | n [] := nil
 | n (x :: xs) := (n, x) :: enumFrom (n + 1) xs
 
-def enum : List α → List (ℕ × α) := enumFrom 0
+def enum : List α → List (Nat × α) := enumFrom 0
 
 def last : Π l : List α, l ≠ [] → α
 | []        h := absurd rfl h
diff --git a/library/init/data/nat/basic.lean b/library/init/data/nat/basic.lean
index b53c4c2daf..95a3f7c009 100644
--- a/library/init/data/nat/basic.lean
+++ b/library/init/data/nat/basic.lean
@@ -84,12 +84,19 @@ instance : HasSub Nat :=
 instance : HasMul Nat :=
 ⟨Nat.mul⟩
 
-@[specialize] def repeatCore {α : Type u} (f : Nat → α → α) (s : Nat) : Nat → α → α
+@[specialize] def forCore {α : Type u} (f : Nat → α → α) (s : Nat) : Nat → α → α
 | 0         a := a
-| (succ n)  a := repeatCore n (f (s - (succ n)) a)
+| (succ n)  a := forCore n (f (s - (succ n)) a)
 
-@[inline] def repeat {α : Type u} (f : Nat → α → α) (n : Nat) (a : α) : α :=
-repeatCore f n n a
+@[inline] def for {α : Type u} (f : Nat → α → α) (n : Nat) (a : α) : α :=
+forCore f n n a
+
+@[specialize] def repeatCore {α : Type u} (f : α → α) : Nat → α → α
+| 0         a := a
+| (succ n)  a := repeatCore n (f a)
+
+@[inline] def repeat {α : Type u} (f : α → α) (n : Nat) (a : α) : α :=
+repeatCore f n a
 
 protected def pow (m : Nat) : Nat → Nat
 | 0        := 1
diff --git a/library/init/data/string/basic.lean b/library/init/data/string/basic.lean
index 06ee6f0106..494c69a588 100644
--- a/library/init/data/string/basic.lean
+++ b/library/init/data/string/basic.lean
@@ -170,7 +170,7 @@ instance : HasAppend String :=
 def str : String → Char → String := push
 
 def pushn (s : String) (c : Char) (n : Nat) : String :=
-n.repeat (λ _ s, s.push c) s
+n.repeat (λ s, s.push c) s
 
 def isEmpty (s : String) : Bool :=
 toBool (s.bsize == 0)