From 7838ed386d8417283d65000a212786c4fa0cf6a7 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 13 Oct 2015 17:01:06 -0700
Subject: [PATCH] refactor(frontends/lean/pp,library/init/reserved_notation):
 pretty print "nat numerals" nicely even when namespace nat is not open

---
 library/init/reserved_notation.lean | 20 ++++++++++----------
 src/frontends/lean/pp.cpp           | 14 +-------------
 2 files changed, 11 insertions(+), 23 deletions(-)

diff --git a/library/init/reserved_notation.lean b/library/init/reserved_notation.lean
index af85e02d9..21ab2e297 100644
--- a/library/init/reserved_notation.lean
+++ b/library/init/reserved_notation.lean
@@ -97,20 +97,20 @@ namespace nat
   protected definition add (a b : nat) : nat :=
   nat.rec a (λ b₁ r, succ r) b
 
-  definition nat_has_zero [reducible] [instance] : has_zero nat :=
-  has_zero.mk nat.zero
-
-  definition nat_has_one [reducible] [instance] : has_one nat :=
-  has_one.mk (nat.succ (nat.zero))
-
-  definition nat_has_add [reducible] [instance] [priority nat.prio] : has_add nat :=
-  has_add.mk nat.add
-
   definition of_num (n : num) : nat :=
   num.rec zero
-    (λ n, pos_num.rec (succ zero) (λ n r, add (add r r) (succ zero)) (λ n r, add r r) n) n
+    (λ n, pos_num.rec (succ zero) (λ n r, nat.add (nat.add r r) (succ zero)) (λ n r, nat.add r r) n) n
 end nat
 
+definition nat_has_zero [reducible] [instance] [priority nat.prio] : has_zero nat :=
+has_zero.mk nat.zero
+
+definition nat_has_one [reducible] [instance] [priority nat.prio] : has_one nat :=
+has_one.mk (nat.succ (nat.zero))
+
+definition nat_has_add [reducible] [instance] [priority nat.prio] : has_add nat :=
+has_add.mk nat.add
+
 /-
   Global declarations of right binding strength
 
diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index 680e7f16e..3872aec59 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -79,14 +79,6 @@ public:
         m_succ(mk_constant(get_nat_succ_name())) {
     }
 
-    // Return ture if the environment has a coercion from num->nat
-    bool has_coercion_num_nat(environment const & env) const {
-        list<expr> coes = get_coercions(env, m_num_type, m_nat);
-        if (length(coes) != 1)
-            return false;
-        return head(coes) == m_nat_of_num;
-    }
-
     // Return an unsigned if \c e if of the form (succ^k zero), and k
     // fits in a machine unsigned integer.
     optional<unsigned> to_unsigned(expr const & e) const {
@@ -109,10 +101,6 @@ public:
 
 static nat_numeral_pp * g_nat_numeral_pp = nullptr;
 
-static bool has_coercion_num_nat(environment const & env) {
-    return g_nat_numeral_pp->has_coercion_num_nat(env);
-}
-
 static optional<unsigned> to_unsigned(expr const & e) {
     return g_nat_numeral_pp->to_unsigned(e);
 }
@@ -292,7 +280,7 @@ void pretty_fn::set_options_core(options const & o) {
     m_abbreviations   = !all && get_pp_abbreviations(o);
     m_preterm         = get_pp_preterm(o);
     m_hide_full_terms = get_formatter_hide_full_terms(o);
-    m_num_nat_coe     = m_numerals && !m_coercion && has_coercion_num_nat(m_env);
+    m_num_nat_coe     = m_numerals && !m_coercion;
 }
 
 void pretty_fn::set_options(options const & o) {