refactor(frontends/lean): remove 'including' expressions

src/emacs/lean-syntax.el

@@ -14,7 +14,7 @@
     "context" "open" "as" "export" "axiom" "inductive" "with" "structure" "universe" "alias" "help" "environment"
     "options" "precedence" "postfix" "prefix" "calc_trans" "calc_subst" "calc_refl"
     "infix" "infixl" "infixr" "notation" "eval" "check" "exit" "coercion" "end"
-    "using" "namespace" "including" "instance" "class" "section"
+    "using" "namespace" "instance" "class" "section"
     "set_option" "add_rewrite" "extends" "include" "omit")
   "lean keywords")
 

src/frontends/lean/builtin_exprs.cpp

@@ -348,31 +348,6 @@ static expr parse_consume_args_expr(parser & p, unsigned, expr const *, pos_info
     }
 }
 
-static expr parse_including_expr(parser & p, unsigned, expr const *, pos_info const & pos) {
-    buffer<expr> locals;
-    while (!p.curr_is_token(get_comma_tk())) {
-        auto pos = p.pos();
-        name id  = p.check_id_next("invalid 'including', identifier expected");
-        if (auto it = p.get_local(id)) {
-            locals.push_back(*it);
-        } else {
-            throw parser_error(sstream() << "invalid 'including', '" << id << "' is not a local declaraton", pos);
-        }
-    }
-    p.next();
-    parser::local_scope scope(p);
-    buffer<expr> new_locals;
-    for (auto old_l : locals) {
-        binder_info bi = mk_contextual_info(true);
-        expr new_l     = p.save_pos(mk_local(p.mk_fresh_name(), local_pp_name(old_l), mk_as_is(mlocal_type(old_l)), bi), pos);
-        p.add_local(new_l);
-        new_locals.push_back(new_l);
-    }
-    expr r = Fun(new_locals, p.parse_expr(), p);
-    r = p.rec_save_pos(mk_app(r, locals), pos);
-    return r;
-}
-
 static expr parse_sorry(parser & p, unsigned, expr const *, pos_info const & pos) {
     return p.mk_sorry(pos);
 }
@@ -411,7 +386,6 @@ parse_table init_nud_table() {
     r = r.add({transition("begin", mk_ext_action(parse_begin_end))}, x0);
     r = r.add({transition("proof", mk_ext_action(parse_proof_qed))}, x0);
     r = r.add({transition("sorry", mk_ext_action(parse_sorry))}, x0);
-    r = r.add({transition("including", mk_ext_action(parse_including_expr))}, x0);
     return r;
 }
 

src/frontends/lean/token_table.cpp

@@ -75,7 +75,7 @@ void init_token_table(token_table & t) {
          {"using", 0}, {"|", 0}, {"!", g_max_prec}, {"with", 0}, {"...", 0}, {",", 0},
          {".", 0}, {":", 0}, {"::", 0}, {"calc", 0}, {":=", 0}, {"--", 0}, {"#", 0},
          {"(*", 0}, {"/-", 0}, {"begin", g_max_prec}, {"proof", g_max_prec}, {"qed", 0}, {"@", g_max_prec},
-         {"including", 0}, {"sorry", g_max_prec}, {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec},
+         {"sorry", g_max_prec}, {"+", g_plus_prec}, {g_cup, g_cup_prec}, {"->", g_arrow_prec},
          {nullptr, 0}};
 
     char const * commands[] =

tests/lean/run/class3.lean

@@ -9,8 +9,8 @@ section
   -- The section mechanism only includes parameters that are explicitly cited.
   -- So, we use the 'including' expression to make explicit we want to use
   -- Ha and Hb
+  include Ha Hb
   theorem tst : inhabited (Prop × A × B)
-  := including Ha Hb, _
 
 end
 

tests/lean/run/tactic30.lean

@@ -7,8 +7,9 @@ section
   parameter  {A : Type}
   parameters {a b : A}
   parameter  H : a = b
+  include H
   theorem test : a = b ∧ a = a
-  := including H, by apply and.intro; assumption; apply eq.refl
+  := by apply and.intro; assumption; apply eq.refl
 end
 
 check @test