From d8548369e71f345c2d3325796c8ba729997d30de Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 29 Aug 2014 07:46:40 -0700
Subject: [PATCH] feat(frontends/lean/pp): improve let-expr pretty printer

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/elaborator.cpp |  5 +++--
 src/frontends/lean/pp.cpp         |  2 ++
 tests/lean/let3.lean              | 15 +++++++++++++++
 tests/lean/let3.lean.expected.out |  1 +
 4 files changed, 21 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/let3.lean
 create mode 100644 tests/lean/let3.lean.expected.out

diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index b4f1233b0..3c57e2978 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -1097,9 +1097,10 @@ public:
             return p->first;
         } else {
             auto ecs = visit(get_annotation_arg(e));
-            m_cache.insert(e, mk_pair(ecs.first, ecs.second));
+            expr r = copy_tag(ecs.first, mk_let_value_annotation(ecs.first));
+            m_cache.insert(e, mk_pair(r, ecs.second));
             cs += ecs.second;
-            return ecs.first;
+            return r;
         }
     }
 
diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index 8e4c9c683..7b6d0db0d 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -324,6 +324,7 @@ static bool is_show(expr const & e) {
     return is_show_annotation(e) && is_app(get_annotation_arg(e)) &&
         is_lambda(app_fn(get_annotation_arg(e)));
 }
+static bool is_let_value(expr const & e) { return is_let_value_annotation(e); }
 
 auto pretty_fn::pp_have(expr const & e) -> result {
     expr proof   = app_arg(e);
@@ -430,6 +431,7 @@ auto pretty_fn::pp(expr const & e) -> result {
     if (is_have(e))         return pp_have(e);
     if (is_let(e))          return pp_let(e);
     if (is_typed_expr(e))   return pp(get_typed_expr_expr(e));
+    if (is_let_value(e))    return pp(get_annotation_arg(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));
diff --git a/tests/lean/let3.lean b/tests/lean/let3.lean
new file mode 100644
index 000000000..83dd47078
--- /dev/null
+++ b/tests/lean/let3.lean
@@ -0,0 +1,15 @@
+import data.num
+using num
+
+variable f : num → num → num → num
+
+check
+  let a := 10
+  in f a 10
+
+/-
+check
+  let a := 10,
+      b := 10
+  in f a b 10
+-/
diff --git a/tests/lean/let3.lean.expected.out b/tests/lean/let3.lean.expected.out
new file mode 100644
index 000000000..607da73ee
--- /dev/null
+++ b/tests/lean/let3.lean.expected.out
@@ -0,0 +1 @@
+let a := 10 in f a 10 : num → num