From 147436bfb869d7c2bf18d2548431ca3e2e00e7ef Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Fri, 5 Jan 2018 10:52:58 -0500 Subject: [PATCH] fix(init/data/nat/lemmas): generalize nat.iterate to (Sort u) --- library/init/data/nat/lemmas.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/init/data/nat/lemmas.lean b/library/init/data/nat/lemmas.lean index 6ce04f9696..34b93c5850 100644 --- 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)