feat(frontends/lean): add tactic_notation command

This addresses the first part of issue #461

We still need support for tactic definitions

hott/init/tactic.hlean

@@ -96,15 +96,14 @@ opaque definition change (e : expr) : tactic := builtin
 
 opaque definition assert_hypothesis (id : identifier) (e : expr) : tactic := builtin
 
-infixl `;`:15 := and_then
+definition try         (t : tactic) : tactic := or_else t id
-notation `(` h `|` r:(foldl `|` (e r, or_else r e) h) `)` := r
+definition repeat1     (t : tactic) : tactic := and_then t (repeat t)
-
-definition try         (t : tactic) : tactic := (t | id)
-definition repeat1     (t : tactic) : tactic := t ; repeat t
 definition focus       (t : tactic) : tactic := focus_at t 0
 definition determ      (t : tactic) : tactic := at_most t 1
-definition trivial                  : tactic := ( apply eq.refl | assumption )
+definition trivial                  : tactic := or_else (apply eq.refl) assumption
 definition do (n : num) (t : tactic) : tactic :=
-nat.rec id (λn t', (t;t')) (nat.of_num n)
+nat.rec id (λn t', and_then t t') (nat.of_num n)
 
 end tactic
+tactic_infixl `;`:15 := tactic.and_then
+tactic_notation `(` h `|` r:(foldl `|` (e r, tactic.or_else r e) h) `)` := r

library/init/tactic.lean

@@ -96,15 +96,13 @@ opaque definition change (e : expr) : tactic := builtin
 
 opaque definition assert_hypothesis (id : identifier) (e : expr) : tactic := builtin
 
-infixl `;`:15 := and_then
+definition try         (t : tactic) : tactic := or_else t id
-notation `(` h `|` r:(foldl `|` (e r, or_else r e) h) `)` := r
+definition repeat1     (t : tactic) : tactic := and_then t (repeat t)
-
-definition try         (t : tactic) : tactic := (t | id)
-definition repeat1     (t : tactic) : tactic := t ; repeat t
 definition focus       (t : tactic) : tactic := focus_at t 0
 definition determ      (t : tactic) : tactic := at_most t 1
-definition trivial                  : tactic := (apply eq.refl | apply true.intro | assumption)
+definition trivial                  : tactic := or_else (or_else (apply eq.refl) (apply true.intro)) assumption
 definition do (n : num) (t : tactic) : tactic :=
-nat.rec id (λn t', (t;t')) (nat.of_num n)
+nat.rec id (λn t', and_then t t') (nat.of_num n)
-
 end tactic
+tactic_infixl `;`:15 := tactic.and_then
+tactic_notation `(` h `|` r:(foldl `|` (e r, tactic.or_else r e) h) `)` := r

src/emacs/lean-syntax.el

@@ -13,9 +13,11 @@
     "hypothesis" "lemma" "corollary" "variable" "variables" "premise" "premises"
     "print" "theorem" "example" "abbreviation"
     "open" "as" "export" "axiom" "axioms" "inductive" "with" "structure" "record" "universe" "universes"
-    "alias" "help" "environment" "options" "precedence" "reserve" "postfix" "prefix"
+    "alias" "help" "environment" "options" "precedence" "reserve"
     "calc_trans" "calc_subst" "calc_refl" "calc_symm" "match"
-    "infix" "infixl" "infixr" "notation" "eval" "check" "coercion" "end"
+    "infix" "infixl" "infixr" "notation" "postfix" "prefix"
+    "tactic_infix" "tactic_infixl" "tactic_infixr" "tactic_notation" "tactic_postfix" "tactic_prefix"
+    "eval" "check" "coercion" "end"
     "using" "namespace" "section" "fields" "find_decl"
     "attribute" "local" "set_option" "add_rewrite" "extends" "include" "omit" "classes"
     "instances" "coercions" "metaclasses" "raw" "migrate" "replacing")

src/frontends/lean/CMakeLists.txt

@@ -7,7 +7,7 @@ begin_end_ext.cpp tactic_hint.cpp pp.cpp theorem_queue.cpp
 structure_cmd.cpp info_manager.cpp info_annotation.cpp find_cmd.cpp
 coercion_elaborator.cpp info_tactic.cpp
 init_module.cpp elaborator_context.cpp calc_proof_elaborator.cpp
-parse_tactic_location.cpp parse_rewrite_tactic.cpp
+parse_tactic_location.cpp parse_rewrite_tactic.cpp builtin_tactics.cpp
 type_util.cpp elaborator_exception.cpp migrate_cmd.cpp local_ref_info.cpp)
 
 target_link_libraries(lean_frontend ${LEAN_LIBS})

src/frontends/lean/builtin_exprs.cpp

@@ -32,7 +32,6 @@ Author: Leonardo de Moura
 #include "frontends/lean/info_tactic.h"
 #include "frontends/lean/info_annotation.h"
 #include "frontends/lean/structure_cmd.h"
-#include "frontends/lean/parse_rewrite_tactic.h"
 
 namespace lean {
 namespace notation {
@@ -521,22 +520,6 @@ static expr parse_calc_expr(parser & p, unsigned, expr const *, pos_info const &
     return parse_calc(p);
 }
 
-static expr parse_rewrite_tactic_expr(parser & p, unsigned, expr const *, pos_info const & pos) {
-    return p.save_pos(parse_rewrite_tactic(p), pos);
-}
-
-static expr parse_esimp_tactic_expr(parser & p, unsigned, expr const *, pos_info const & pos) {
-    return p.save_pos(parse_esimp_tactic(p), pos);
-}
-
-static expr parse_unfold_tactic_expr(parser & p, unsigned, expr const *, pos_info const & pos) {
-    return p.save_pos(parse_unfold_tactic(p), pos);
-}
-
-static expr parse_fold_tactic_expr(parser & p, unsigned, expr const *, pos_info const & pos) {
-    return p.save_pos(parse_fold_tactic(p), pos);
-}
-
 static expr parse_overwrite_notation(parser & p, unsigned, expr const *, pos_info const &) {
     name n = p.check_id_next("invalid '#' local notation, identifier expected");
     environment env = overwrite_notation(p.env(), n);
@@ -607,10 +590,6 @@ parse_table init_nud_table() {
     r = r.add({transition("Type", mk_ext_action(parse_Type))}, x0);
     r = r.add({transition("let", mk_ext_action(parse_let_expr))}, x0);
     r = r.add({transition("calc", mk_ext_action(parse_calc_expr))}, x0);
-    r = r.add({transition("rewrite", mk_ext_action(parse_rewrite_tactic_expr))}, x0);
-    r = r.add({transition("esimp", mk_ext_action(parse_esimp_tactic_expr))}, x0);
-    r = r.add({transition("unfold", mk_ext_action(parse_unfold_tactic_expr))}, x0);
-    r = r.add({transition("fold", mk_ext_action(parse_fold_tactic_expr))}, x0);
     r = r.add({transition("#", mk_ext_action(parse_overwrite_notation))}, x0);
     r = r.add({transition("@", mk_ext_action(parse_explicit_expr))}, x0);
     r = r.add({transition("!", mk_ext_action(parse_consume_args_expr))}, x0);

src/frontends/lean/init_module.cpp

@@ -15,6 +15,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/begin_end_ext.h"
 #include "frontends/lean/builtin_cmds.h"
 #include "frontends/lean/builtin_exprs.h"
+#include "frontends/lean/builtin_tactics.h"
 #include "frontends/lean/inductive_cmd.h"
 #include "frontends/lean/structure_cmd.h"
 #include "frontends/lean/migrate_cmd.h"
@@ -37,6 +38,7 @@ void initialize_frontend_lean_module() {
     initialize_parse_table();
     initialize_builtin_cmds();
     initialize_builtin_exprs();
+    initialize_builtin_tactics();
     initialize_elaborator_context();
     initialize_elaborator();
     initialize_scanner();
@@ -75,6 +77,7 @@ void finalize_frontend_lean_module() {
     finalize_scanner();
     finalize_elaborator();
     finalize_elaborator_context();
+    finalize_builtin_tactics();
     finalize_builtin_exprs();
     finalize_builtin_cmds();
     finalize_parse_table();

src/frontends/lean/notation_cmd.cpp

@@ -96,7 +96,7 @@ void check_not_forbidden(char const * tk) {
     }
 }
 
-static auto parse_mixfix_notation(parser & p, mixfix_kind k, bool overload, bool reserve, bool parse_only)
+static auto parse_mixfix_notation(parser & p, mixfix_kind k, bool overload, notation_entry_group grp, bool parse_only)
 -> pair<notation_entry, optional<token_entry>> {
     std::string tk = parse_symbol(p, "invalid notation declaration, quoted symbol or identifier expected");
     char const * tks = tk.c_str();
@@ -107,7 +107,7 @@ static auto parse_mixfix_notation(parser & p, mixfix_kind k, bool overload, bool
 
     optional<parse_table> reserved_pt;
     optional<action> reserved_action;
-    if (!reserve) {
+    if (grp != notation_entry_group::Reserve) {
         if (k == mixfix_kind::prefix) {
             if (auto at = get_reserved_nud_table(p.env()).find(tks)) {
                 reserved_pt     = at->second;
@@ -178,7 +178,7 @@ static auto parse_mixfix_notation(parser & p, mixfix_kind k, bool overload, bool
         }
     }
 
-    if (reserve) {
+    if (grp == notation_entry_group::Reserve) {
         // reserve notation commands do not have a denotation
         expr dummy = mk_Prop();
         if (p.curr_is_token(get_assign_tk()))
@@ -186,16 +186,16 @@ static auto parse_mixfix_notation(parser & p, mixfix_kind k, bool overload, bool
         switch (k) {
         case mixfix_kind::infixl:
             return mk_pair(notation_entry(false, to_list(transition(tks, mk_expr_action(*prec))),
-                                          dummy, overload, reserve, parse_only), new_token);
+                                          dummy, overload, grp, parse_only), new_token);
         case mixfix_kind::infixr:
             return mk_pair(notation_entry(false, to_list(transition(tks, mk_expr_action(*prec))),
-                                          dummy, overload, reserve, parse_only), new_token);
+                                          dummy, overload, grp, parse_only), new_token);
         case mixfix_kind::postfix:
             return mk_pair(notation_entry(false, to_list(transition(tks, mk_skip_action())),
-                                          dummy, overload, reserve, parse_only), new_token);
+                                          dummy, overload, grp, parse_only), new_token);
         case mixfix_kind::prefix:
             return mk_pair(notation_entry(true, to_list(transition(tks, mk_expr_action(*prec))),
-                                          dummy, overload, reserve, parse_only), new_token);
+                                          dummy, overload, grp, parse_only), new_token);
         }
     } else {
         p.check_token_next(get_assign_tk(), "invalid notation declaration, ':=' expected");
@@ -207,25 +207,25 @@ static auto parse_mixfix_notation(parser & p, mixfix_kind k, bool overload, bool
 #if defined(__GNUC__) && !defined(__CLANG__)
 #pragma GCC diagnostic ignored "-Wmaybe-uninitialized"
             return mk_pair(notation_entry(false, to_list(transition(tks, mk_expr_action(*prec))),
-                                          mk_app(f, Var(1), Var(0)), overload, reserve, parse_only), new_token);
+                                          mk_app(f, Var(1), Var(0)), overload, grp, parse_only), new_token);
 #endif
         case mixfix_kind::infixr:
             return mk_pair(notation_entry(false, to_list(transition(tks, mk_expr_action(*prec))),
-                                          mk_app(f, Var(1), Var(0)), overload, reserve, parse_only), new_token);
+                                          mk_app(f, Var(1), Var(0)), overload, grp, parse_only), new_token);
         case mixfix_kind::postfix:
             return mk_pair(notation_entry(false, to_list(transition(tks, mk_skip_action())),
-                                          mk_app(f, Var(0)), overload, reserve, parse_only), new_token);
+                                          mk_app(f, Var(0)), overload, grp, parse_only), new_token);
         case mixfix_kind::prefix:
             return mk_pair(notation_entry(true, to_list(transition(tks, mk_expr_action(*prec))),
-                                          mk_app(f, Var(0)), overload, reserve, parse_only), new_token);
+                                          mk_app(f, Var(0)), overload, grp, parse_only), new_token);
         }
     }
     lean_unreachable(); // LCOV_EXCL_LINE
 }
 
-static notation_entry parse_mixfix_notation(parser & p, mixfix_kind k, bool overload, bool reserve,
+static notation_entry parse_mixfix_notation(parser & p, mixfix_kind k, bool overload, notation_entry_group grp,
                                             buffer<token_entry> & new_tokens, bool parse_only) {
-    auto nt = parse_mixfix_notation(p, k, overload, reserve, parse_only);
+    auto nt = parse_mixfix_notation(p, k, overload, grp, parse_only);
     if (nt.second)
         new_tokens.push_back(*nt.second);
     return nt.first;
@@ -416,7 +416,7 @@ static unsigned parse_binders_rbp(parser & p) {
     }
 }
 
-static notation_entry parse_notation_core(parser & p, bool overload, bool reserve, buffer<token_entry> & new_tokens, bool parse_only) {
+static notation_entry parse_notation_core(parser & p, bool overload, notation_entry_group grp, buffer<token_entry> & new_tokens, bool parse_only) {
     buffer<expr>       locals;
     buffer<transition> ts;
     parser::local_scope scope(p);
@@ -436,16 +436,16 @@ static notation_entry parse_notation_core(parser & p, bool overload, bool reserv
         parse_notation_local(p, locals);
         is_nud = false;
         pt = get_led_table(p.env());
-        if (!reserve)
+        if (grp != notation_entry_group::Reserve)
             reserved_pt = get_reserved_led_table(p.env());
     } else {
         pt = get_nud_table(p.env());
-        if (!reserve)
+        if (grp != notation_entry_group::Reserve)
             reserved_pt = get_reserved_nud_table(p.env());
     }
     bool used_default = false;
-    while ((!reserve && !p.curr_is_token(get_assign_tk())) ||
+    while ((grp != notation_entry_group::Reserve && !p.curr_is_token(get_assign_tk())) ||
-           (reserve && !p.curr_is_command() && !p.curr_is_eof())) {
+           (grp == notation_entry_group::Reserve && !p.curr_is_command() && !p.curr_is_eof())) {
         name tk = parse_quoted_symbol_or_token(p, new_tokens, used_default);
         if (auto at = find_next(reserved_pt, tk)) {
             action const & a = at->first;
@@ -521,7 +521,7 @@ static notation_entry parse_notation_core(parser & p, bool overload, bool reserv
         new_tokens.back().m_prec = get_max_prec();
     }
     expr n;
-    if (reserve) {
+    if (grp == notation_entry_group::Reserve) {
         // reserve notation commands do not have a denotation
         lean_assert(p.curr_is_command() || p.curr_is_eof());
         expr dummy = mk_Prop(); // any expression without free variables will do
@@ -533,7 +533,7 @@ static notation_entry parse_notation_core(parser & p, bool overload, bool reserv
             throw parser_error("invalid notation declaration, empty notation is not allowed", p.pos());
         n = parse_notation_expr(p, locals);
     }
-    return notation_entry(is_nud, to_list(ts.begin(), ts.end()), n, overload, reserve, parse_only);
+    return notation_entry(is_nud, to_list(ts.begin(), ts.end()), n, overload, grp, parse_only);
 }
 
 bool curr_is_notation_decl(parser & p) {
@@ -542,25 +542,25 @@ bool curr_is_notation_decl(parser & p) {
         p.curr_is_token(get_postfix_tk()) || p.curr_is_token(get_prefix_tk()) || p.curr_is_token(get_notation_tk());
 }
 
-static notation_entry parse_notation(parser & p, bool overload, bool reserve, buffer<token_entry> & new_tokens,
+static notation_entry parse_notation(parser & p, bool overload, notation_entry_group grp, buffer<token_entry> & new_tokens,
                                      bool allow_local) {
     bool parse_only = false;
     flet<bool> set_allow_local(g_allow_local, allow_local);
     if (p.curr_is_token(get_infix_tk()) || p.curr_is_token(get_infixl_tk())) {
         p.next();
-        return parse_mixfix_notation(p, mixfix_kind::infixl, overload, reserve, new_tokens, parse_only);
+        return parse_mixfix_notation(p, mixfix_kind::infixl, overload, grp, new_tokens, parse_only);
     } else if (p.curr_is_token(get_infixr_tk())) {
         p.next();
-        return parse_mixfix_notation(p, mixfix_kind::infixr, overload, reserve, new_tokens, parse_only);
+        return parse_mixfix_notation(p, mixfix_kind::infixr, overload, grp, new_tokens, parse_only);
     } else if (p.curr_is_token(get_postfix_tk())) {
         p.next();
-        return parse_mixfix_notation(p, mixfix_kind::postfix, overload, reserve, new_tokens, parse_only);
+        return parse_mixfix_notation(p, mixfix_kind::postfix, overload, grp, new_tokens, parse_only);
     } else if (p.curr_is_token(get_prefix_tk())) {
         p.next();
-        return parse_mixfix_notation(p, mixfix_kind::prefix, overload, reserve, new_tokens, parse_only);
+        return parse_mixfix_notation(p, mixfix_kind::prefix, overload, grp, new_tokens, parse_only);
     } else if (p.curr_is_token(get_notation_tk())) {
         p.next();
-        return parse_notation_core(p, overload, reserve, new_tokens, parse_only);
+        return parse_notation_core(p, overload, grp, new_tokens, parse_only);
     } else {
         throw parser_error("invalid notation, 'infix', 'infixl', 'infixr', 'prefix', "
                            "'postfix' or 'notation' expected", p.pos());
@@ -568,8 +568,8 @@ static notation_entry parse_notation(parser & p, bool overload, bool reserve, bu
 }
 
 notation_entry parse_notation(parser & p, bool overload, buffer<token_entry> & new_tokens, bool allow_local) {
-    bool reserve = false;
+    notation_entry_group grp = notation_entry_group::Main;
-    return parse_notation(p, overload, reserve, new_tokens, allow_local);
+    return parse_notation(p, overload, grp, new_tokens, allow_local);
 }
 
 static char g_reserved_chars[] = {'(', ')', ',', 0};
@@ -624,24 +624,24 @@ struct notation_modifiers {
     }
 };
 
-static environment notation_cmd_core(parser & p, bool overload, bool reserve, bool persistent) {
+static environment notation_cmd_core(parser & p, bool overload, notation_entry_group grp, bool persistent) {
     notation_modifiers mods;
     mods.parse(p);
     flet<bool> set_allow_local(g_allow_local, !persistent);
     environment env = p.env();
     buffer<token_entry> new_tokens;
-    auto ne = parse_notation_core(p, overload, reserve, new_tokens, mods.m_parse_only);
+    auto ne = parse_notation_core(p, overload, grp, new_tokens, mods.m_parse_only);
     for (auto const & te : new_tokens)
         env = add_user_token(env, te, persistent);
     env = add_notation(env, ne, persistent);
     return env;
 }
 
-static environment mixfix_cmd(parser & p, mixfix_kind k, bool overload, bool reserve, bool persistent) {
+static environment mixfix_cmd(parser & p, mixfix_kind k, bool overload, notation_entry_group grp, bool persistent) {
     notation_modifiers mods;
     mods.parse(p);
     flet<bool> set_allow_local(g_allow_local, !persistent);
-    auto nt = parse_mixfix_notation(p, k, overload, reserve, mods.m_parse_only);
+    auto nt = parse_mixfix_notation(p, k, overload, grp, mods.m_parse_only);
     environment env = p.env();
     if (nt.second)
         env = add_user_token(env, *nt.second, persistent);
@@ -651,59 +651,94 @@ static environment mixfix_cmd(parser & p, mixfix_kind k, bool overload, bool res
 
 static environment notation_cmd(parser & p) {
     bool overload = true;
-    bool reserve  = false;
+    notation_entry_group grp = notation_entry_group::Main;
     bool persistent = true;
-    return notation_cmd_core(p, overload, reserve, persistent);
+    return notation_cmd_core(p, overload, grp, persistent);
 }
 
 static environment infixl_cmd(parser & p) {
     bool overload = true;
-    bool reserve  = false;
+    notation_entry_group grp = notation_entry_group::Main;
     bool persistent = true;
-    return mixfix_cmd(p, mixfix_kind::infixl, overload, reserve, persistent);
+    return mixfix_cmd(p, mixfix_kind::infixl, overload, grp, persistent);
 }
 
 static environment infixr_cmd(parser & p) {
     bool overload = true;
-    bool reserve  = false;
+    notation_entry_group grp = notation_entry_group::Main;
     bool persistent = true;
-    return mixfix_cmd(p, mixfix_kind::infixr, overload, reserve, persistent);
+    return mixfix_cmd(p, mixfix_kind::infixr, overload, grp, persistent);
 }
 
 static environment postfix_cmd(parser & p) {
     bool overload = true;
-    bool reserve  = false;
+    notation_entry_group grp = notation_entry_group::Main;
     bool persistent = true;
-    return mixfix_cmd(p, mixfix_kind::postfix, overload, reserve, persistent);
+    return mixfix_cmd(p, mixfix_kind::postfix, overload, grp, persistent);
 }
 
 static environment prefix_cmd(parser & p) {
     bool overload = true;
-    bool reserve  = false;
+    notation_entry_group grp = notation_entry_group::Main;
     bool persistent = true;
-    return mixfix_cmd(p, mixfix_kind::prefix, overload, reserve, persistent);
+    return mixfix_cmd(p, mixfix_kind::prefix, overload, grp, persistent);
+}
+
+static environment tactic_notation_cmd(parser & p) {
+    bool overload = false;
+    notation_entry_group grp = notation_entry_group::Tactic;
+    bool persistent = true;
+    return notation_cmd_core(p, overload, grp, persistent);
+}
+
+static environment tactic_infixl_cmd(parser & p) {
+    bool overload = false;
+    notation_entry_group grp = notation_entry_group::Tactic;
+    bool persistent = true;
+    return mixfix_cmd(p, mixfix_kind::infixl, overload, grp, persistent);
+}
+
+static environment tactic_infixr_cmd(parser & p) {
+    bool overload = false;
+    notation_entry_group grp = notation_entry_group::Tactic;
+    bool persistent = true;
+    return mixfix_cmd(p, mixfix_kind::infixr, overload, grp, persistent);
+}
+
+static environment tactic_postfix_cmd(parser & p) {
+    bool overload = false;
+    notation_entry_group grp = notation_entry_group::Tactic;
+    bool persistent = true;
+    return mixfix_cmd(p, mixfix_kind::postfix, overload, grp, persistent);
+}
+
+static environment tactic_prefix_cmd(parser & p) {
+    bool overload = false;
+    notation_entry_group grp = notation_entry_group::Tactic;
+    bool persistent = true;
+    return mixfix_cmd(p, mixfix_kind::prefix, overload, grp, persistent);
 }
 
 // auxiliary procedure used by local_notation_cmd and reserve_cmd
-static environment dispatch_notation_cmd(parser & p, bool overload, bool reserve, bool persistent) {
+static environment dispatch_notation_cmd(parser & p, bool overload, notation_entry_group grp, bool persistent) {
     if (p.curr_is_token(get_notation_tk())) {
         p.next();
-        return notation_cmd_core(p, overload, reserve, persistent);
+        return notation_cmd_core(p, overload, grp, persistent);
     } else if (p.curr_is_token(get_infixl_tk())) {
         p.next();
-        return mixfix_cmd(p, mixfix_kind::infixl, overload, reserve, persistent);
+        return mixfix_cmd(p, mixfix_kind::infixl, overload, grp, persistent);
     } else if (p.curr_is_token(get_infix_tk())) {
         p.next();
-        return mixfix_cmd(p, mixfix_kind::infixl, overload, reserve, persistent);
+        return mixfix_cmd(p, mixfix_kind::infixl, overload, grp, persistent);
     } else if (p.curr_is_token(get_infixr_tk())) {
         p.next();
-        return mixfix_cmd(p, mixfix_kind::infixr, overload, reserve, persistent);
+        return mixfix_cmd(p, mixfix_kind::infixr, overload, grp, persistent);
     } else if (p.curr_is_token(get_prefix_tk())) {
         p.next();
-        return mixfix_cmd(p, mixfix_kind::prefix, overload, reserve, persistent);
+        return mixfix_cmd(p, mixfix_kind::prefix, overload, grp, persistent);
     } else if (p.curr_is_token(get_postfix_tk())) {
         p.next();
-        return mixfix_cmd(p, mixfix_kind::postfix, overload, reserve, persistent);
+        return mixfix_cmd(p, mixfix_kind::postfix, overload, grp, persistent);
     } else {
         throw parser_error("invalid local/reserve notation, 'infix', 'infixl', 'infixr', 'prefix', "
                            "'postfix' or 'notation' expected", p.pos());
@@ -712,16 +747,16 @@ static environment dispatch_notation_cmd(parser & p, bool overload, bool reserve
 
 environment local_notation_cmd(parser & p) {
     bool overload   = false; // REMARK: local notation override global one
-    bool reserve    = false;
+    notation_entry_group grp = notation_entry_group::Main;
     bool persistent = false;
-    return dispatch_notation_cmd(p, overload, reserve, persistent);
+    return dispatch_notation_cmd(p, overload, grp, persistent);
 }
 
 static environment reserve_cmd(parser & p) {
     bool overload   = false;
-    bool reserve    = true;
+    notation_entry_group grp = notation_entry_group::Reserve;
     bool persistent = true;
-    return dispatch_notation_cmd(p, overload, reserve, persistent);
+    return dispatch_notation_cmd(p, overload, grp, persistent);
 }
 
 static environment precedence_cmd(parser & p) {
@@ -732,13 +767,19 @@ static environment precedence_cmd(parser & p) {
 }
 
 void register_notation_cmds(cmd_table & r) {
-    add_cmd(r, cmd_info("precedence",   "set token left binding power", precedence_cmd));
+    add_cmd(r, cmd_info("precedence",      "set token left binding power", precedence_cmd));
-    add_cmd(r, cmd_info("infixl",       "declare a new infix (left) notation", infixl_cmd));
+    add_cmd(r, cmd_info("infixl",          "declare a new infix (left) notation", infixl_cmd));
-    add_cmd(r, cmd_info("infix",        "declare a new infix (left) notation", infixl_cmd));
+    add_cmd(r, cmd_info("infix",           "declare a new infix (left) notation", infixl_cmd));
-    add_cmd(r, cmd_info("infixr",       "declare a new infix (right) notation", infixr_cmd));
+    add_cmd(r, cmd_info("infixr",          "declare a new infix (right) notation", infixr_cmd));
-    add_cmd(r, cmd_info("postfix",      "declare a new postfix notation", postfix_cmd));
+    add_cmd(r, cmd_info("postfix",         "declare a new postfix notation", postfix_cmd));
-    add_cmd(r, cmd_info("prefix",       "declare a new prefix notation", prefix_cmd));
+    add_cmd(r, cmd_info("prefix",          "declare a new prefix notation", prefix_cmd));
-    add_cmd(r, cmd_info("notation",     "declare a new notation", notation_cmd));
+    add_cmd(r, cmd_info("notation",        "declare a new notation", notation_cmd));
-    add_cmd(r, cmd_info("reserve",      "reserve notation", reserve_cmd));
+    add_cmd(r, cmd_info("tactic_infixl",   "declare a new tactic infix (left) notation", tactic_infixl_cmd));
+    add_cmd(r, cmd_info("tactic_infix",    "declare a new tactic infix (left) notation", tactic_infixl_cmd));
+    add_cmd(r, cmd_info("tactic_infixr",   "declare a new tactic infix (right) notation", tactic_infixr_cmd));
+    add_cmd(r, cmd_info("tactic_postfix",  "declare a new tactic postfix notation", tactic_postfix_cmd));
+    add_cmd(r, cmd_info("tactic_prefix",   "declare a new tactic prefix notation", tactic_prefix_cmd));
+    add_cmd(r, cmd_info("tactic_notation", "declare a new tacitc notation", tactic_notation_cmd));
+    add_cmd(r, cmd_info("reserve",         "reserve notation", reserve_cmd));
 }
 }

src/frontends/lean/parser.cpp

@@ -925,7 +925,7 @@ bool parser::parse_local_notation_decl(buffer<notation_entry> * nentries) {
     }
 }
 
-expr parser::parse_notation(parse_table t, expr * left) {
+expr parser::parse_notation_core(parse_table t, expr * left, bool as_tactic) {
     lean_assert(curr() == scanner::token_kind::Keyword);
     auto p = pos();
     if (m_info_manager)
@@ -949,17 +949,17 @@ expr parser::parse_notation(parse_table t, expr * left) {
             break;
         case notation::action_kind::Expr:
             next();
-            args.push_back(parse_expr(a.rbp()));
+            args.push_back(parse_expr_or_tactic(a.rbp(), as_tactic));
             break;
         case notation::action_kind::Exprs: {
             next();
             buffer<expr> r_args;
             auto terminator = a.get_terminator();
             if (!terminator || !curr_is_token(*terminator)) {
-                r_args.push_back(parse_expr(a.rbp()));
+                r_args.push_back(parse_expr_or_tactic(a.rbp(), as_tactic));
                 while (curr_is_token(a.get_sep())) {
                     next();
-                    r_args.push_back(parse_expr(a.rbp()));
+                    r_args.push_back(parse_expr_or_tactic(a.rbp(), as_tactic));
                 }
             }
             if (terminator) {
@@ -1473,34 +1473,18 @@ expr parser::parse_tactic_nud() {
         } else {
             return parse_expr();
         }
-    } else if (curr_is_token_or_id(get_rewrite_tk())) {
+    } else if (curr_is_keyword()) {
-        auto p = pos();
+        return parse_tactic_notation(tactic_nud(), nullptr);
-        next();
-        return save_pos(parse_rewrite_tactic(*this), p);
-    } else if (curr_is_token(get_lparen_tk())) {
-        next();
-        expr r = parse_tactic();
-        while (curr_is_token(get_bar_tk())) {
-            auto bar_pos = pos();
-            next();
-            expr n = parse_tactic();
-            r = mk_app({save_pos(mk_constant(get_tactic_or_else_name()), bar_pos), r, n}, bar_pos);
-        }
-        check_token_next(get_rparen_tk(), "invalid tactic, ')' expected");
-        return r;
     } else {
-        return parse_expr();
+        throw parser_error("invalid tactic expression", pos());
     }
 }
 
 expr parser::parse_tactic_led(expr left) {
-    auto p = pos();
+    if (tactic_led().find(get_token_info().value())) {
-    if (curr_is_token(get_semicolon_tk())) {
+        return parse_tactic_notation(tactic_led(), &left);
-        next();
-        expr right = parse_tactic();
-        return mk_app({save_pos(mk_constant(get_tactic_and_then_name()), p), left, right}, p);
     } else {
-        return parse_led(left);
+        throw parser_error("invalid tactic expression", pos());
     }
 }
 

src/frontends/lean/parser.h

@@ -169,6 +169,8 @@ class parser {
 
     parse_table const & nud() const { return get_nud_table(env()); }
     parse_table const & led() const { return get_led_table(env()); }
+    parse_table const & tactic_nud() const { return get_tactic_nud_table(env()); }
+    parse_table const & tactic_led() const { return get_tactic_led_table(env()); }
 
     unsigned curr_level_lbp() const;
     level parse_max_imax(bool is_max);
@@ -181,7 +183,12 @@ class parser {
     void parse_script(bool as_expr = false);
     bool parse_commands();
     unsigned curr_lbp() const;
-    expr parse_notation(parse_table t, expr * left);
+    expr parse_notation_core(parse_table t, expr * left, bool as_tactic);
+    expr parse_expr_or_tactic(unsigned rbp, bool as_tactic) {
+        return as_tactic ? parse_tactic(rbp) : parse_expr(rbp);
+    }
+    expr parse_notation(parse_table t, expr * left) { return parse_notation_core(t, left, false); }
+    expr parse_tactic_notation(parse_table t, expr * left) { return parse_notation_core(t, left, true); }
     expr parse_nud_notation();
     expr parse_led_notation(expr left);
     expr parse_nud();

src/frontends/lean/parser_config.cpp

@@ -11,6 +11,7 @@ Author: Leonardo de Moura
 #include "library/kernel_serializer.h"
 #include "frontends/lean/parser_config.h"
 #include "frontends/lean/builtin_exprs.h"
+#include "frontends/lean/builtin_tactics.h"
 #include "frontends/lean/builtin_cmds.h"
 
 namespace lean {
@@ -24,22 +25,23 @@ notation_entry replace(notation_entry const & e, std::function<expr(expr const &
     else
         return notation_entry(e.is_nud(),
                               map(e.get_transitions(), [&](transition const & t) { return notation::replace(t, f); }),
-                              f(e.get_expr()), e.overload(), e.reserve(), e.parse_only());
+                              f(e.get_expr()), e.overload(), e.group(), e.parse_only());
 }
 
 notation_entry::notation_entry():m_kind(notation_entry_kind::NuD) {}
 notation_entry::notation_entry(notation_entry const & e):
     m_kind(e.m_kind), m_expr(e.m_expr), m_overload(e.m_overload),
-    m_safe_ascii(e.m_safe_ascii), m_reserve(e.m_reserve), m_parse_only(e.m_parse_only) {
+    m_safe_ascii(e.m_safe_ascii), m_group(e.m_group), m_parse_only(e.m_parse_only) {
     if (is_numeral())
         new (&m_num) mpz(e.m_num);
     else
         new (&m_transitions) list<transition>(e.m_transitions);
 }
 
-notation_entry::notation_entry(bool is_nud, list<transition> const & ts, expr const & e, bool overload, bool reserve, bool parse_only):
+notation_entry::notation_entry(bool is_nud, list<transition> const & ts, expr const & e, bool overload,
+                               notation_entry_group g, bool parse_only):
     m_kind(is_nud ? notation_entry_kind::NuD : notation_entry_kind::LeD),
-    m_expr(e), m_overload(overload), m_reserve(reserve), m_parse_only(parse_only) {
+    m_expr(e), m_overload(overload), m_group(g), m_parse_only(parse_only) {
     new (&m_transitions) list<transition>(ts);
     m_safe_ascii = std::all_of(ts.begin(), ts.end(), [](transition const & t) { return t.is_safe_ascii(); });
 }
@@ -48,7 +50,7 @@ notation_entry::notation_entry(notation_entry const & e, bool overload):
     m_overload = overload;
 }
 notation_entry::notation_entry(mpz const & val, expr const & e, bool overload, bool parse_only):
-    m_kind(notation_entry_kind::Numeral), m_expr(e), m_overload(overload), m_safe_ascii(true), m_reserve(false), m_parse_only(parse_only) {
+    m_kind(notation_entry_kind::Numeral), m_expr(e), m_overload(overload), m_safe_ascii(true), m_group(notation_entry_group::Main), m_parse_only(parse_only) {
     new (&m_num) mpz(val);
 }
 
@@ -61,7 +63,7 @@ notation_entry::~notation_entry() {
 
 bool operator==(notation_entry const & e1, notation_entry const & e2) {
     if (e1.kind() != e2.kind() || e1.overload() != e2.overload() || e1.get_expr() != e2.get_expr() ||
-        e1.reserve() != e2.reserve() || e1.parse_only() != e2.parse_only())
+        e1.group() != e2.group() || e1.parse_only() != e2.parse_only())
         return false;
     if (e1.is_numeral())
         return e1.get_num() == e2.get_num();
@@ -213,11 +215,34 @@ struct notation_state {
     // The following two tables are used to implement `reserve notation` commands
     parse_table      m_reserved_nud;
     parse_table      m_reserved_led;
+    // The following two tables are used to implement `notation [tactic]` commands
+    parse_table      m_tactic_nud;
+    parse_table      m_tactic_led;
     notation_state():
         m_nud(get_builtin_nud_table()),
         m_led(get_builtin_led_table()),
         m_reserved_nud(true),
-        m_reserved_led(false) {
+        m_reserved_led(false),
+        m_tactic_nud(get_builtin_tactic_nud_table()),
+        m_tactic_led(get_builtin_tactic_led_table()) {
+    }
+
+    parse_table & nud(notation_entry_group g) {
+        switch (g) {
+        case notation_entry_group::Main:    return m_nud;
+        case notation_entry_group::Reserve: return m_reserved_nud;
+        case notation_entry_group::Tactic:  return m_tactic_nud;
+        }
+        lean_unreachable();
+    }
+
+    parse_table & led(notation_entry_group g) {
+        switch (g) {
+        case notation_entry_group::Main:    return m_led;
+        case notation_entry_group::Reserve: return m_reserved_led;
+        case notation_entry_group::Tactic:  return m_tactic_led;
+        }
+        lean_unreachable();
     }
 };
 
@@ -239,7 +264,7 @@ struct notation_config {
             to_buffer(e.get_transitions(), ts);
             if (auto idx = get_head_index(ts.size(), ts.data(), e.get_expr()))
                 updt_inv_map(s, *idx, e);
-            parse_table & nud = e.reserve() ? s.m_reserved_nud : s.m_nud;
+            parse_table & nud = s.nud(e.group());
             nud = nud.add(ts.size(), ts.data(), e.get_expr(), e.overload());
             break;
         }
@@ -247,7 +272,7 @@ struct notation_config {
             to_buffer(e.get_transitions(), ts);
             if (auto idx = get_head_index(ts.size(), ts.data(), e.get_expr()))
                 updt_inv_map(s, *idx, e);
-            parse_table & led = e.reserve() ? s.m_reserved_led : s.m_led;
+            parse_table & led = s.led(e.group());
             led = led.add(ts.size(), ts.data(), e.get_expr(), e.overload());
             break;
         }
@@ -275,7 +300,7 @@ struct notation_config {
         if (e.is_numeral()) {
             s << e.get_num();
         } else {
-            s << e.reserve() << length(e.get_transitions());
+            s << static_cast<char>(e.group()) << length(e.get_transitions());
             for (auto const & t : e.get_transitions())
                 s << t;
         }
@@ -290,13 +315,13 @@ struct notation_config {
             return entry(val, e, overload, parse_only);
         } else {
             bool is_nud = k == notation_entry_kind::NuD;
-            bool reserve;
+            unsigned sz; char _g;
-            unsigned sz;
+            d >> _g >> sz;
-            d >> reserve >> sz;
+            notation_entry_group g = static_cast<notation_entry_group>(_g);
             buffer<transition> ts;
             for (unsigned i = 0; i < sz; i++)
                 ts.push_back(read_transition(d));
-            return entry(is_nud, to_list(ts.begin(), ts.end()), e, overload, reserve, parse_only);
+            return entry(is_nud, to_list(ts.begin(), ts.end()), e, overload, g, parse_only);
         }
     }
     static optional<unsigned> get_fingerprint(entry const &) {
@@ -314,25 +339,25 @@ environment add_notation(environment const & env, notation_entry const & e, bool
 }
 
 environment add_nud_notation(environment const & env, unsigned num, notation::transition const * ts,
-                             expr const & a, bool overload, bool reserve, bool parse_only) {
+                             expr const & a, bool overload, notation_entry_group g, bool parse_only) {
-    return add_notation(env, notation_entry(true, to_list(ts, ts+num), a, overload, reserve, parse_only));
+    return add_notation(env, notation_entry(true, to_list(ts, ts+num), a, overload, g, parse_only));
 }
 
 environment add_led_notation(environment const & env, unsigned num, notation::transition const * ts,
-                             expr const & a, bool overload, bool reserve, bool parse_only) {
+                             expr const & a, bool overload, notation_entry_group g, bool parse_only) {
-    return add_notation(env, notation_entry(false, to_list(ts, ts+num), a, overload, reserve, parse_only));
+    return add_notation(env, notation_entry(false, to_list(ts, ts+num), a, overload, g, parse_only));
 }
 
 environment add_nud_notation(environment const & env, std::initializer_list<notation::transition> const & ts,
                              expr const & a, bool overload, bool parse_only) {
-    bool reserve = false;
+    notation_entry_group g = notation_entry_group::Main;
-    return add_nud_notation(env, ts.size(), ts.begin(), a, overload, reserve, parse_only);
+    return add_nud_notation(env, ts.size(), ts.begin(), a, overload, g, parse_only);
 }
 
 environment add_led_notation(environment const & env, std::initializer_list<notation::transition> const & ts,
                              expr const & a, bool overload, bool parse_only) {
-    bool reserve = false;
+    notation_entry_group g = notation_entry_group::Main;
-    return add_led_notation(env, ts.size(), ts.begin(), a, overload, reserve, parse_only);
+    return add_led_notation(env, ts.size(), ts.begin(), a, overload, g, parse_only);
 }
 
 parse_table const & get_nud_table(environment const & env) {
@@ -351,6 +376,14 @@ parse_table const & get_reserved_led_table(environment const & env) {
     return notation_ext::get_state(env).m_reserved_led;
 }
 
+parse_table const & get_tactic_nud_table(environment const & env) {
+    return notation_ext::get_state(env).m_tactic_nud;
+}
+
+parse_table const & get_tactic_led_table(environment const & env) {
+    return notation_ext::get_state(env).m_tactic_led;
+}
+
 environment add_mpz_notation(environment const & env, mpz const & n, expr const & e, bool overload, bool parse_only) {
     return add_notation(env, notation_entry(n, e, overload, parse_only));
 }

src/frontends/lean/parser_config.h

@@ -19,7 +19,7 @@ struct token_entry {
 };
 
 enum class notation_entry_kind { NuD, LeD, Numeral };
-
+enum class notation_entry_group { Main, Reserve, Tactic };
 class notation_entry {
     typedef notation::transition transition;
     notation_entry_kind  m_kind;
@@ -30,12 +30,12 @@ class notation_entry {
     expr                 m_expr;
     bool                 m_overload;
     bool                 m_safe_ascii;
-    bool                 m_reserve;
+    notation_entry_group m_group;
     bool                 m_parse_only;
 public:
     notation_entry();
     notation_entry(notation_entry const & e);
-    notation_entry(bool is_nud, list<transition> const & ts, expr const & e, bool overload, bool reserve, bool parse_only);
+    notation_entry(bool is_nud, list<transition> const & ts, expr const & e, bool overload, notation_entry_group g, bool parse_only);
     notation_entry(mpz const & val, expr const & e, bool overload, bool parse_only);
     notation_entry(notation_entry const & e, bool overload);
     ~notation_entry();
@@ -47,7 +47,8 @@ public:
     expr const & get_expr() const { return m_expr; }
     bool overload() const { return m_overload; }
     bool is_safe_ascii() const { return m_safe_ascii; }
-    bool reserve() const { return m_reserve; }
+    notation_entry_group group() const { return m_group; }
+    bool reserve() const { return group() == notation_entry_group::Reserve; }
     bool parse_only() const { return m_parse_only; }
 };
 bool operator==(notation_entry const & e1, notation_entry const & e2);
@@ -63,9 +64,9 @@ environment add_notation(environment const & env, notation_entry const & e, bool
 
 environment add_token(environment const & env, char const * val, unsigned prec);
 environment add_nud_notation(environment const & env, unsigned num, notation::transition const * ts, expr const & a,
-                             bool overload = true, bool reserve = false, bool parse_only = false);
+                             bool overload = true, notation_entry_group g = notation_entry_group::Main, bool parse_only = false);
 environment add_led_notation(environment const & env, unsigned num, notation::transition const * ts, expr const & a,
-                             bool overload = true, bool reserve = false, bool parse_only = false);
+                             bool overload = true, notation_entry_group g = notation_entry_group::Main, bool parse_only = false);
 environment add_nud_notation(environment const & env, std::initializer_list<notation::transition> const & ts, expr const & a,
                              bool overload = true, bool parse_only = false);
 environment add_led_notation(environment const & env, std::initializer_list<notation::transition> const & ts, expr const & a,
@@ -75,6 +76,8 @@ parse_table const & get_nud_table(environment const & env);
 parse_table const & get_led_table(environment const & env);
 parse_table const & get_reserved_nud_table(environment const & env);
 parse_table const & get_reserved_led_table(environment const & env);
+parse_table const & get_tactic_nud_table(environment const & env);
+parse_table const & get_tactic_led_table(environment const & env);
 cmd_table const & get_cmd_table(environment const & env);
 /** \brief Force notation from namespace \c n to shadow any existing notation */
 environment overwrite_notation(environment const & env, name const & n);

src/frontends/lean/token_table.cpp

@@ -97,6 +97,7 @@ void init_token_table(token_table & t) {
          "end", "namespace", "section", "prelude", "help",
          "import", "inductive", "record", "structure", "module", "universe", "universes", "local",
          "precedence", "reserve", "infixl", "infixr", "infix", "postfix", "prefix", "notation",
+         "tactic_infixl", "tactic_infixr", "tactic_infix", "tactic_postfix", "tactic_prefix", "tactic_notation",
          "exit", "set_option", "open", "export", "calc_subst", "calc_refl", "calc_trans", "calc_symm", "tactic_hint",
          "add_begin_end_tactic", "set_begin_end_tactic", "instance", "class",
          "multiple_instances", "find_decl", "attribute", "persistent",

tests/lean/errors.lean.expected.out

@@ -1,7 +1,6 @@
 errors.lean:4:0: error: unknown identifier 'a'
 tst1 : nat → nat → nat
-errors.lean:12:2: error: function expected at
+errors.lean:12:12: error: invalid tactic expression
-  tactic.cases [tactic.expr add] tactic.expr_list.nil
 errors.lean:22:12: error: unknown identifier 'b'
 tst3 : A → A → A
 foo.tst1 : ℕ → ℕ → ℕ

tests/lean/run/all_goals2.lean

@@ -4,12 +4,15 @@ open nat
 attribute nat.add [unfold-c 2]
 attribute nat.rec_on [unfold-c 2]
 
+infixl `;`:15 := tactic.and_then
+
 namespace tactic
   definition then_all (t1 t2 : tactic) : tactic :=
   focus (t1 ; all_goals t2)
-  infixl `;;`:15 := tactic.then_all
 end tactic
 
+tactic_infixl `;;`:15 := tactic.then_all
+
 open tactic
 example (a b c : nat) : (a + 0 = 0 + a ∧ b + 0 = 0 + b) ∧ c = c :=
 

tests/lean/run/by_exact.lean

@@ -0,0 +1,5 @@
+import data.nat
+open nat
+
+example (a b c : nat) (h₁ : a + 0 = b) (h₂ : b = c) : a = c :=
+by esimp at h₁; rewrite h₂ at h₁; exact h₁

tests/lean/run/def_tac.lean

@@ -1,3 +1,5 @@
+infixl `;`:15 := tactic.and_then
+
 section
   open tactic
   definition cases_refl (e : expr) : tactic :=
@@ -12,7 +14,7 @@ section
   cases e expr_list.nil; apply rfl
 end
 
-notation `cases_lst` l:(foldr `,` (h t, tactic.expr_list.cons h t) tactic.expr_list.nil) := cases_lst_refl l
+tactic_notation `cases_lst` l:(foldr `,` (h t, tactic.expr_list.cons h t) tactic.expr_list.nil) := cases_lst_refl l
 
 open prod
 theorem tst₁ (a : nat × nat) : (pr1 a, pr2 a) = a :=

tests/lean/run/tac1.lean

@@ -1,6 +1,9 @@
 import logic
 open tactic
 
+notation `(` h `|` r:(foldl `|` (e r, tactic.or_else r e) h) `)` := r
+infixl `;`:15 := tactic.and_then
+
 definition mytac := apply @and.intro; apply @eq.refl
 
 check @mytac

tests/lean/run/tactic14.lean

@@ -1,6 +1,8 @@
 import logic
 open tactic
 
+notation `(` h `|` r:(foldl `|` (e r, tactic.or_else r e) h) `)` := r
+
 definition basic_tac : tactic
 := repeat (apply @and.intro | assumption)
 

tests/lean/run/tactic20.lean

@@ -1,6 +1,8 @@
 import logic
 open tactic
 
+infixl `;`:15 := tactic.and_then
+
 definition assump := eassumption
 
 theorem tst {A : Type} {a b c : A} (H1 : a = b) (H2 : b = c) : a = c

tests/lean/run/tactic21.lean

@@ -1,13 +1,11 @@
 import logic
 open tactic
 
-definition assump := eassumption
-
 theorem tst1 {A : Type} {a b c : A} {p : A → A → Prop} (H1 : p a b) (H2 : p b c) : ∃ x, p a x ∧ p x c
-:= by apply exists.intro; apply and.intro; assump; assump
+:= by apply exists.intro; apply and.intro; eassumption; eassumption
 
 theorem tst2 {A : Type} {a b c d : A} {p : A → A → Prop} (Ha : p a c) (H1 : p a b) (Hb : p b d) (H2 : p b c) : ∃ x, p a x ∧ p x c
-:= by apply exists.intro; apply and.intro; assump; assump
+:= by apply exists.intro; apply and.intro; eassumption; eassumption
 
 (*
 print(get_env():find("tst2"):value())

tests/lean/run/tactic22.lean

@@ -1,5 +1,9 @@
 import logic
 open tactic
 
+notation `(` h `|` r:(foldl `|` (e r, tactic.or_else r e) h) `)` := r
+infixl `;`:15 := tactic.and_then
+
+
 theorem T (a b c d : Prop) (Ha : a) (Hb : b) (Hc : c) (Hd : d) : a ∧ b ∧ c ∧ d
-:= by fixpoint (λ f, (apply @and.intro; f | assumption; f | id))
+:= by fixpoint (λ f, (apply and.intro; f | assumption; f | id))

tests/lean/run/tactic24.lean

@@ -1,6 +1,9 @@
 import logic
 open tactic
 
+notation `(` h `|` r:(foldl `|` (e r, tactic.or_else r e) h) `)` := r
+infixl `;`:15 := tactic.and_then
+
 definition my_tac1 := apply @eq.refl
 definition my_tac2 := repeat (apply @and.intro; assumption)
 

tests/lean/run/tactic25.lean

@@ -2,7 +2,7 @@ import logic
 open tactic
 
 definition my_tac1 := apply @eq.refl
-definition my_tac2 := repeat (apply @and.intro; assumption)
+definition my_tac2 := repeat (and_then (apply and.intro) assumption)
 
 tactic_hint my_tac1
 tactic_hint my_tac2
@@ -11,8 +11,11 @@ theorem T1 {A : Type.{2}} (a : A) : a = a
 
 theorem T2 {a b c : Prop} (Ha : a) (Hb : b) (Hc : c) : a ∧ b ∧ c
 
-definition my_tac3 := fixpoint (λ f, (apply @or.intro_left; f  |
+notation `(` h `|` r:(foldl `|` (e r, tactic.or_else r e) h) `)` := r
-                                      apply @or.intro_right; f |
+infixl `;`:15 := tactic.and_then
+
+definition my_tac3 := fixpoint (λ f, (apply or.intro_left; f  |
+                                      apply or.intro_right; f |
                                       assumption))
 
 tactic_hint my_tac3

tests/lean/run/tactic26.lean

@@ -12,6 +12,9 @@ theorem inl_inhabited {A : Type} (B : Type) (H : inhabited A) : inhabited (sum A
 theorem inr_inhabited (A : Type) {B : Type} (H : inhabited B) : inhabited (sum A B)
 := inhabited.destruct H (λ b, inhabited.mk (sum.inr A b))
 
+notation `(` h `|` r:(foldl `|` (e r, tactic.or_else r e) h) `)` := r
+infixl `;`:15 := tactic.and_then
+
 definition my_tac := fixpoint (λ t, ( apply @inl_inhabited; t
                                     | apply @inr_inhabited; t
                                     | apply @num.is_inhabited

tests/lean/run/tactic27.lean

@@ -1,6 +1,8 @@
 import logic
 open tactic
 
+notation `(` h `|` r:(foldl `|` (e r, tactic.or_else r e) h) `)` := r
+
 definition my_tac := repeat (apply @and.intro | apply @eq.refl)
 tactic_hint my_tac
 

tests/lean/run/tactic28.lean

@@ -14,6 +14,9 @@ theorem inr_inhabited (A : Type) {B : Type} (H : inhabited B) : inhabited (sum A
 
 infixl `..`:10 := append
 
+notation `(` h `|` r:(foldl `|` (e r, tactic.or_else r e) h) `)` := r
+infixl `;`:15 := tactic.and_then
+
 definition my_tac := repeat (trace "iteration"; state;
                               (  apply @inl_inhabited; trace "used inl"
                               .. apply @inr_inhabited; trace "used inr"

tests/lean/run/tactic4.lean

@@ -3,10 +3,7 @@ open tactic (renaming id->id_tac)
 
 definition id {A : Type} (a : A) := a
 
-definition simple {A : Prop} : tactic
-:= unfold id; assumption
-
 theorem tst {A B : Prop} (H1 : A) (H2 : B) : id A
-:= by simple
+:= by unfold id; assumption
 
 check tst

tests/lean/run/tactic5.lean

@@ -3,7 +3,9 @@ open tactic (renaming id->id_tac)
 
 definition id {A : Type} (a : A) := a
 
+infixl `;`:15 := tactic.and_then
+
 theorem tst {A B : Prop} (H1 : A) (H2 : B) : id A
-:= by !(unfold id; state); assumption
+:= by (unfold id; state); assumption
 
 check tst

tests/lean/run/tactic7.lean

@@ -2,7 +2,7 @@ import logic
 open tactic
 
 theorem tst {A B : Prop} (H1 : A) (H2 : B) : A ∧ B ∧ A
-:= by apply and.intro; state; assumption; apply and.intro; !assumption
+:= by apply and.intro; state; assumption; apply and.intro; assumption
 check tst
 
 theorem tst2 {A B : Prop} (H1 : A) (H2 : B) : A ∧ B ∧ A

tests/lean/run/tactic9.lean

@@ -2,4 +2,4 @@ import logic
 open tactic
 
 theorem tst {A B : Prop} (H1 : A) (H2 : B) : ((fun x : Prop, x) A) ∧ B ∧ A
-:= by apply and.intro; beta; assumption; apply and.intro; !assumption
+:= by apply and.intro; beta; assumption; apply and.intro; assumption