From e8454fad26b1f4a123fc167a83c52144660804ce Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 12 Oct 2015 17:03:03 -0700 Subject: [PATCH] fix(library/data/real/basic): remove obsolete notation declarations --- library/data/real/basic.lean | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/library/data/real/basic.lean b/library/data/real/basic.lean index e6e9002fd..c54263929 100644 --- a/library/data/real/basic.lean +++ b/library/data/real/basic.lean @@ -26,8 +26,6 @@ open algebra open - [coercions] rat local postfix `⁻¹` := pnat.inv -local notation 0 := rat.of_num 0 -local notation 1 := rat.of_num 1 -- small helper lemmas @@ -631,7 +629,7 @@ private theorem mul_bound_helper {s t : seq} (Hs : regular s) (Ht : regular t) ( apply rat.le.trans, apply mul_le_mul_of_nonneg_right, apply pceil_helper Hn, - { repeat (apply algebra.mul_pos | apply algebra.add_pos | apply rat_of_pnat_is_pos | + { repeat (apply algebra.mul_pos | apply algebra.add_pos | apply rat_of_pnat_is_pos | apply pnat.inv_pos) }, apply rat.le_of_lt, apply add_pos,