fix(init/data/nat/lemmas): generalize nat.iterate to (Sort u)

2018-01-05 10:52:58 -05:00 · 2018-01-05 10:52:58 -05:00 · 147436bfb8
commit 147436bfb8
parent 6635f6c8c1
1 changed files with 1 additions and 1 deletions
--- a/library/init/data/nat/lemmas.lean
+++ b/library/init/data/nat/lemmas.lean
@ -874,7 +874,7 @@ begin
  apply le_div_iff_mul_le _ _ Hk
 end

-def iterate {α : Type} (op : α → α) : ℕ → α → α
+def iterate {α : Sort u} (op : α → α) : ℕ → α → α
 | 0        a := a
 | (succ k) a := iterate k (op a)