From 8ce992b0772592a1aa8c47780e07a4291149b0de Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 19 May 2015 16:26:02 -0700
Subject: [PATCH] feat(frontends/lean/builtin_exprs): allow 'obtain' to be used
 in tactic mode

---
 src/frontends/lean/builtin_exprs.cpp | 3 ++-
 src/frontends/lean/tokens.cpp        | 4 ++++
 src/frontends/lean/tokens.h          | 1 +
 src/frontends/lean/tokens.txt        | 1 +
 tests/lean/run/obtain_tac.lean       | 6 ++++++
 5 files changed, 14 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/obtain_tac.lean

diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp
index eac15967b7..24b76def95 100644
--- a/src/frontends/lean/builtin_exprs.cpp
+++ b/src/frontends/lean/builtin_exprs.cpp
@@ -230,7 +230,8 @@ static expr parse_begin_end_core(parser & p, pos_info const & pos, name const &
                 }
             } else if (p.curr_is_token(get_match_tk()) || p.curr_is_token(get_assume_tk()) ||
                        p.curr_is_token(get_take_tk())  || p.curr_is_token(get_fun_tk()) ||
-                       p.curr_is_token(get_calc_tk())  || p.curr_is_token(get_show_tk())) {
+                       p.curr_is_token(get_calc_tk())  || p.curr_is_token(get_show_tk()) ||
+                       p.curr_is_token(get_obtain_tk())) {
                 auto pos = p.pos();
                 expr t = p.parse_tactic_expr_arg();
                 t      = p.mk_app(get_exact_tac_fn(), t, pos);
diff --git a/src/frontends/lean/tokens.cpp b/src/frontends/lean/tokens.cpp
index 2665438e17..520c1e3a76 100644
--- a/src/frontends/lean/tokens.cpp
+++ b/src/frontends/lean/tokens.cpp
@@ -130,6 +130,7 @@ static name const * g_prefix_tk = nullptr;
 static name const * g_notation_tk = nullptr;
 static name const * g_call_tk = nullptr;
 static name const * g_calc_tk = nullptr;
+static name const * g_obtain_tk = nullptr;
 static name const * g_persistent_tk = nullptr;
 static name const * g_root_tk = nullptr;
 static name const * g_fields_tk = nullptr;
@@ -264,6 +265,7 @@ void initialize_tokens() {
     g_notation_tk = new name{"notation"};
     g_call_tk = new name{"call"};
     g_calc_tk = new name{"calc"};
+    g_obtain_tk = new name{"obtain"};
     g_persistent_tk = new name{"[persistent]"};
     g_root_tk = new name{"_root_"};
     g_fields_tk = new name{"fields"};
@@ -399,6 +401,7 @@ void finalize_tokens() {
     delete g_notation_tk;
     delete g_call_tk;
     delete g_calc_tk;
+    delete g_obtain_tk;
     delete g_persistent_tk;
     delete g_root_tk;
     delete g_fields_tk;
@@ -533,6 +536,7 @@ name const & get_prefix_tk() { return *g_prefix_tk; }
 name const & get_notation_tk() { return *g_notation_tk; }
 name const & get_call_tk() { return *g_call_tk; }
 name const & get_calc_tk() { return *g_calc_tk; }
+name const & get_obtain_tk() { return *g_obtain_tk; }
 name const & get_persistent_tk() { return *g_persistent_tk; }
 name const & get_root_tk() { return *g_root_tk; }
 name const & get_fields_tk() { return *g_fields_tk; }
diff --git a/src/frontends/lean/tokens.h b/src/frontends/lean/tokens.h
index 4727ed68fb..042ffb3cb4 100644
--- a/src/frontends/lean/tokens.h
+++ b/src/frontends/lean/tokens.h
@@ -132,6 +132,7 @@ name const & get_prefix_tk();
 name const & get_notation_tk();
 name const & get_call_tk();
 name const & get_calc_tk();
+name const & get_obtain_tk();
 name const & get_persistent_tk();
 name const & get_root_tk();
 name const & get_fields_tk();
diff --git a/src/frontends/lean/tokens.txt b/src/frontends/lean/tokens.txt
index b41a17c873..051fc70c70 100644
--- a/src/frontends/lean/tokens.txt
+++ b/src/frontends/lean/tokens.txt
@@ -125,6 +125,7 @@ prefix       prefix
 notation     notation
 call         call
 calc         calc
+obtain       obtain
 persistent   [persistent]
 root         _root_
 fields       fields
diff --git a/tests/lean/run/obtain_tac.lean b/tests/lean/run/obtain_tac.lean
new file mode 100644
index 0000000000..fff5fd55b1
--- /dev/null
+++ b/tests/lean/run/obtain_tac.lean
@@ -0,0 +1,6 @@
+example (a b : Prop) : a ∧ b → b ∧ a :=
+begin
+  intro Hab,
+  obtain Ha Hb, from Hab,
+  show b ∧ a, from and.intro Hb Ha
+end