From c6d44d2e4976b264ef3220772b4e12f88fb0f55b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 8 Sep 2016 16:31:42 -0700 Subject: [PATCH] chore(library/init/nat): fix style --- library/init/nat.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/library/init/nat.lean b/library/init/nat.lean index fae22dcef7..d55b7c5024 100644 --- a/library/init/nat.lean +++ b/library/init/nat.lean @@ -173,10 +173,10 @@ namespace nat le_of_succ_le H theorem succ_le_succ {n m : ℕ} : n ≤ m → succ n ≤ succ m := - le.rec (nat.le_refl (succ n)) (λa b, le.step) + le.rec (nat.le_refl (succ n)) (λ a b, le.step) theorem pred_le_pred {n m : ℕ} : n ≤ m → pred n ≤ pred m := - le.rec (nat.le_refl (pred n)) (nat.rec (λa b, b) (λa b c, le.step)) + le.rec (nat.le_refl (pred n)) (nat.rec (λ a b, b) (λ a b c, le.step)) theorem le_of_succ_le_succ {n m : ℕ} : succ n ≤ succ m → n ≤ m := pred_le_pred