diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 522369252..0021ccb92 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -105,7 +105,7 @@ environment variable_cmd_core(parser & p, bool is_axiom, binder_info const & bi) } type = p.elaborate(type, ls); if (in_section(p.env())) { - p.add_local_expr(n, p.save_pos(mk_local(n, n, type), pos), bi); + p.add_local_expr(n, p.save_pos(mk_local(n, type), pos), bi); return p.env(); } else { environment env = p.env(); diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index fbc31f1d5..a91f79e03 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -75,7 +75,7 @@ static expr parse_let(parser & p, pos_info const & pos) { type = p.pi_abstract(ps, type); value = p.lambda_abstract(ps, value); } - expr l = p.save_pos(mk_local(id, id, type), pos); + expr l = p.save_pos(mk_local(id, type), pos); p.add_local(l); expr body = abstract(parse_let_body(p, pos), l); return p.save_pos(mk_let(id, type, value, body), pos); diff --git a/src/frontends/lean/notation_cmd.cpp b/src/frontends/lean/notation_cmd.cpp index 0159ff2f3..ad50a4b01 100644 --- a/src/frontends/lean/notation_cmd.cpp +++ b/src/frontends/lean/notation_cmd.cpp @@ -136,7 +136,7 @@ static void parse_notation_local(parser & p, buffer & locals) { if (p.curr_is_identifier()) { name n = p.get_name_val(); p.next(); - expr l = mk_local(n, n, g_local_type); // remark: the type doesn't matter + expr l = mk_local(n, g_local_type); // remark: the type doesn't matter p.add_local_expr(n, l); locals.push_back(l); } else { @@ -221,7 +221,7 @@ environment notation_cmd_core(parser & p, bool overload) { name n = p.get_name_val(); p.next(); action a = parse_action(p, env, locals); - expr l = mk_local(n, n, g_local_type); + expr l = mk_local(n, g_local_type); p.add_local_expr(n, l); locals.push_back(l); ts.push_back(transition(tk, a)); diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 18469de7d..4be0fcfa0 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -496,7 +496,7 @@ parameter parser::parse_binder_core(binder_info const & bi) { } else { type = save_pos(mk_expr_placeholder(), p); } - return parameter(p, save_pos(mk_local(id, id, type), p), bi); + return parameter(p, save_pos(mk_local(id, type), p), bi); } parameter parser::parse_binder() { @@ -538,7 +538,7 @@ void parser::parse_binder_block(buffer & r, binder_info const & bi) { } for (auto p : names) { expr arg_type = type ? *type : save_pos(mk_expr_placeholder(), p.first); - expr local = save_pos(mk_local(p.second, p.second, arg_type), p.first); + expr local = save_pos(mk_local(p.second, arg_type), p.first); add_local(local); r.push_back(parameter(p.first, local, bi)); } diff --git a/src/kernel/expr.h b/src/kernel/expr.h index 70f0f6ac5..a924a4aa7 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -436,6 +436,7 @@ inline expr Const(name const & n) { return mk_constant(n); } expr mk_macro(macro_definition const & m, unsigned num = 0, expr const * args = nullptr); expr mk_metavar(name const & n, expr const & t); expr mk_local(name const & n, name const & pp_n, expr const & t); +inline expr mk_local(name const & n, expr const & t) { return mk_local(n, n, t); } expr mk_app(expr const & f, expr const & a); expr mk_app(expr const & f, unsigned num_args, expr const * args); expr mk_app(unsigned num_args, expr const * args); diff --git a/src/kernel/formatter.cpp b/src/kernel/formatter.cpp index d598c18ae..353b01c5a 100644 --- a/src/kernel/formatter.cpp +++ b/src/kernel/formatter.cpp @@ -33,14 +33,14 @@ name pick_unused_name(expr const & t, name const & s) { std::pair binding_body_fresh(expr const & b, bool preserve_type) { lean_assert(is_binding(b)); name n = pick_unused_name(binding_body(b), binding_name(b)); - expr c = mk_local(n, n, preserve_type ? binding_domain(b) : expr()); + expr c = mk_local(n, preserve_type ? binding_domain(b) : expr()); return mk_pair(instantiate(binding_body(b), c), c); } std::pair let_body_fresh(expr const & l, bool preserve_type) { lean_assert(is_let(l)); name n = pick_unused_name(let_body(l), let_name(l)); - expr c = mk_local(n, n, preserve_type ? let_type(l) : expr()); + expr c = mk_local(n, preserve_type ? let_type(l) : expr()); return mk_pair(instantiate(let_body(l), c), c); } diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp index 5c6127e4b..4a5f7f3ee 100644 --- a/src/library/kernel_bindings.cpp +++ b/src/library/kernel_bindings.cpp @@ -512,7 +512,7 @@ static int expr_mk_local(lua_State * L) { int nargs = lua_gettop(L); name n = to_name_ext(L, 1); if (nargs == 2) - return push_expr(L, mk_local(n, n, to_expr(L, 2))); + return push_expr(L, mk_local(n, to_expr(L, 2))); else return push_expr(L, mk_local(n, to_name_ext(L, 2), to_expr(L, 3))); } diff --git a/src/tests/kernel/environment.cpp b/src/tests/kernel/environment.cpp index d95f252b9..1ad4ee135 100644 --- a/src/tests/kernel/environment.cpp +++ b/src/tests/kernel/environment.cpp @@ -60,7 +60,7 @@ static void tst1() { auto env3 = add_decl(env2, mk_definition("id", level_param_names(), Pi(A, mk_Type(), A >> A), Fun({{A, mk_Type()}, {x, A}}, x))); - expr c = mk_local("c", "c", Bool); + expr c = mk_local("c", Bool); expr id = Const("id"); type_checker checker(env3, name_generator("tmp")); lean_assert(checker.check(id(Bool)) == Bool >> Bool); @@ -91,8 +91,8 @@ static void tst2() { expr f97 = Const(name(base, 97)); expr f98 = Const(name(base, 98)); expr f3 = Const(name(base, 3)); - expr c1 = mk_local("c1", "c1", Bool); - expr c2 = mk_local("c2", "c2", Bool); + expr c1 = mk_local("c1", Bool); + expr c2 = mk_local("c2", Bool); expr id = Const("id"); std::cout << checker.whnf(f3(c1, c2)) << "\n"; lean_assert_eq(env.find(name(base, 98))->get_weight(), 98); diff --git a/src/tests/kernel/expr.cpp b/src/tests/kernel/expr.cpp index fd763763b..ccc9e3fc0 100644 --- a/src/tests/kernel/expr.cpp +++ b/src/tests/kernel/expr.cpp @@ -349,7 +349,7 @@ static void tst18() { expr f = Const("f"); expr x = Var(0); expr a = Const("a"); - expr l = mk_local("m", "m", Bool); + expr l = mk_local("m", Bool); expr m = mk_metavar("m", Bool); check_serializer(l); lean_assert(!has_local(m));