feat(frontends/lean/pp): pretty print numerals

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/frontends/lean/pp.cpp

@@ -15,6 +15,7 @@ Author: Leonardo de Moura
 #include "library/placeholder.h"
 #include "library/private.h"
 #include "library/explicit.h"
+#include "library/num.h"
 #include "frontends/lean/pp.h"
 #include "frontends/lean/pp_options.h"
 #include "frontends/lean/token_table.h"
@@ -403,6 +404,10 @@ auto pretty_fn::pp_macro(expr const & e) -> result {
     }
 }
 
+auto pretty_fn::pp_num(mpz const & n) -> result {
+    return mk_result(format(n));
+}
+
 auto pretty_fn::pp(expr const & e) -> result {
     if (m_depth > m_max_depth || m_num_steps > m_max_steps)
         return mk_result(m_unicode ? g_ellipsis_n_fmt : g_ellipsis_fmt);
@@ -413,6 +418,7 @@ auto pretty_fn::pp(expr const & e) -> result {
     if (is_show(e)) return pp_show(e);
     if (is_let(e))  return pp_let(e);
     if (is_have(e)) return pp_have(e);
+    if (auto n = to_num(e)) return pp_num(*n);
     if (!m_metavar_args && is_meta(e)) return pp_meta(get_app_fn(e));
 
     switch (e.kind()) {

src/frontends/lean/pp.h

@@ -70,6 +70,7 @@ private:
     result pp_show(expr const & e);
     result pp_macro(expr const & e);
     result pp_explicit(expr const & e);
+    result pp_num(mpz const & n);
     void set_options_core(options const & o);
 
 public:

tests/lean/num.lean

@@ -0,0 +1,15 @@
+import data.num
+using num
+
+check 10
+check 20
+check 3
+check 1
+check 0
+check 12
+check 13
+check 12138
+check 1221
+check 11
+check 5
+check 21

tests/lean/num.lean.expected.out

@@ -0,0 +1,12 @@
+10 : num
+20 : num
+3 : num
+1 : num
+0 : num
+12 : num
+13 : num
+12138 : num
+1221 : num
+11 : num
+5 : num
+21 : num