feat(frontends/lean/builtin_exprs): allow 'obtain' to be used in tactic mode

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);

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; }

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();

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

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