From 750076111424cbef1ee66243db8f9d49aa17ded2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 3 Sep 2014 16:14:29 -0700 Subject: [PATCH] refactor(library/data/nat/basic): remove unnecessary nat_ Signed-off-by: Leonardo de Moura --- library/data/nat/basic.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/library/data/nat/basic.lean b/library/data/nat/basic.lean index e5c2f0e0e7..e889e19788 100644 --- a/library/data/nat/basic.lean +++ b/library/data/nat/basic.lean @@ -24,9 +24,9 @@ inductive nat : Type := notation `ℕ` := nat -theorem nat_rec_zero {P : ℕ → Type} (x : P zero) (f : ∀m, P m → P (succ m)) : nat_rec x f zero = x +theorem rec_zero {P : ℕ → Type} (x : P zero) (f : ∀m, P m → P (succ m)) : nat_rec x f zero = x -theorem nat_rec_succ {P : ℕ → Type} (x : P zero) (f : ∀m, P m → P (succ m)) (n : ℕ) : +theorem rec_succ {P : ℕ → Type} (x : P zero) (f : ∀m, P m → P (succ m)) (n : ℕ) : nat_rec x f (succ n) = f n (nat_rec x f n) theorem induction_on [protected] {P : ℕ → Prop} (a : ℕ) (H1 : P zero) (H2 : ∀ (n : ℕ) (IH : P n), P (succ n)) :