From f21647899ffb1f76d8c6805509e4a8b50d969642 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 7 Aug 2015 18:25:54 +0100
Subject: [PATCH] feat(frontends/lean/builtin_exprs): rename 'show' hidden name
 to 'this'

This is useful if 'show' is recursive
---
 src/frontends/lean/builtin_exprs.cpp | 8 ++------
 src/frontends/lean/builtin_exprs.h   | 1 -
 tests/lean/run/show2.lean            | 9 +++++++++
 3 files changed, 11 insertions(+), 7 deletions(-)
 create mode 100644 tests/lean/run/show2.lean

diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp
index 185224517..ca57a60b2 100644
--- a/src/frontends/lean/builtin_exprs.cpp
+++ b/src/frontends/lean/builtin_exprs.cpp
@@ -499,16 +499,15 @@ static expr parse_suppose(parser & p, unsigned, expr const *, pos_info const & p
     return p.save_pos(Fun(l, body), pos);
 }
 
-static name * H_show = nullptr;
 static expr parse_show(parser & p, unsigned, expr const *, pos_info const & pos) {
     expr prop  = p.parse_expr();
     if (p.curr_is_token(get_bar_tk())) {
-        expr fn = p.save_pos(mk_local(*H_show, prop), pos);
+        expr fn = p.save_pos(mk_local(get_this_tk(), prop), pos);
         return parse_local_equations(p, fn);
     } else {
         p.check_token_next(get_comma_tk(), "invalid 'show' declaration, ',' expected");
         expr proof = parse_proof(p, prop);
-        expr b = p.save_pos(mk_lambda(*H_show, prop, Var(0)), pos);
+        expr b = p.save_pos(mk_lambda(get_this_tk(), prop, Var(0)), pos);
         expr r = p.mk_app(b, proof, pos);
         return p.save_pos(mk_show_annotation(r), pos);
     }
@@ -717,7 +716,6 @@ parse_table init_led_table() {
     return r;
 }
 }
-bool is_show_aux_name(name const & n) { return n == *notation::H_show; }
 
 static parse_table * g_nud_table = nullptr;
 static parse_table * g_led_table = nullptr;
@@ -731,7 +729,6 @@ parse_table get_builtin_led_table() {
 }
 
 void initialize_builtin_exprs() {
-    notation::H_show        = new name("H_show");
     notation::H_obtain_from = new name("H_obtain_from");
     notation::g_not         = new expr(mk_constant(get_not_name()));
     g_nud_table             = new parse_table();
@@ -743,7 +740,6 @@ void initialize_builtin_exprs() {
 void finalize_builtin_exprs() {
     delete g_led_table;
     delete g_nud_table;
-    delete notation::H_show;
     delete notation::H_obtain_from;
     delete notation::g_not;
 }
diff --git a/src/frontends/lean/builtin_exprs.h b/src/frontends/lean/builtin_exprs.h
index 2928c6893..2e8e846ac 100644
--- a/src/frontends/lean/builtin_exprs.h
+++ b/src/frontends/lean/builtin_exprs.h
@@ -9,7 +9,6 @@ Author: Leonardo de Moura
 namespace lean {
 parse_table get_builtin_nud_table();
 parse_table get_builtin_led_table();
-bool is_show_aux_name(name const & n);
 void initialize_builtin_exprs();
 void finalize_builtin_exprs();
 }
diff --git a/tests/lean/run/show2.lean b/tests/lean/run/show2.lean
new file mode 100644
index 000000000..bac2639eb
--- /dev/null
+++ b/tests/lean/run/show2.lean
@@ -0,0 +1,9 @@
+import data.nat
+open nat
+
+example : ∀ a b, a + b = b + a :=
+show ∀ a b : nat, a + b = b + a
+| 0        0        := rfl
+| 0        (succ b) := by rewrite zero_add
+| (succ a) 0        := by rewrite zero_add
+| (succ a) (succ b) := by rewrite [succ_add, this]