diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index 9f7c17f84..a0a87637b 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -448,7 +448,7 @@ class parser::imp { unsigned i = 0; for (unsigned j = 0; j < imp_args.size(); j++) { if (imp_args[j]) { - new_args.push_back(save(mk_placholder(), pos)); + new_args.push_back(save(mk_placeholder(), pos)); } else { if (i >= num_args) throw parser_error(sstream() << "unexpected number of arguments for denotation with implicit arguments, it expects " << num_args << " explicit argument(s)", pos); @@ -598,7 +598,7 @@ class parser::imp { // get all explicit arguments. for (unsigned i = 0; i < imp_args.size(); i++) { if (imp_args[i]) { - args.push_back(save(mk_placholder(), pos())); + args.push_back(save(mk_placeholder(), pos())); } else { args.push_back(parse_expr(1)); } @@ -763,7 +763,7 @@ class parser::imp { if (type) arg_type = lift_free_vars(type, i); else - arg_type = save(mk_placholder(), names[i].first); + arg_type = save(mk_placeholder(), names[i].first); result[sz + i] = std::make_tuple(names[i].first, names[i].second, arg_type, implicit_decl); } } @@ -960,7 +960,7 @@ class parser::imp { expr parse_placeholder() { auto p = pos(); next(); - return save(mk_placholder(), p); + return save(mk_placeholder(), p); } /** @@ -1184,7 +1184,7 @@ class parser::imp { next(); pre_type = parse_expr(); if (!is_definition && curr_is_period()) { - pre_val = save(mk_placholder(), pos()); + pre_val = save(mk_placeholder(), pos()); } else { check_assign_next("invalid definition, ':=' expected"); pre_val = parse_expr(); @@ -1192,7 +1192,7 @@ class parser::imp { } else if (is_definition && curr_is_assign()) { auto p = pos(); next(); - pre_type = save(mk_placholder(), p); + pre_type = save(mk_placeholder(), p); pre_val = parse_expr(); } else { mk_scope scope(*this); @@ -1201,7 +1201,7 @@ class parser::imp { expr type_body = parse_expr(); pre_type = mk_abstraction(false, bindings, type_body); if (!is_definition && curr_is_period()) { - pre_val = mk_abstraction(true, bindings, mk_placholder()); + pre_val = mk_abstraction(true, bindings, mk_placeholder()); } else { check_assign_next("invalid definition, ':=' expected"); expr val_body = parse_expr(); diff --git a/src/library/placeholder.cpp b/src/library/placeholder.cpp index 2e6fdcd09..5ef37e050 100644 --- a/src/library/placeholder.cpp +++ b/src/library/placeholder.cpp @@ -12,7 +12,7 @@ Author: Leonardo de Moura namespace lean { static name g_placeholder_name("_"); -expr mk_placholder() { +expr mk_placeholder() { return mk_constant(g_placeholder_name); } @@ -21,7 +21,7 @@ bool is_placeholder(expr const & e) { } bool has_placeholder(expr const & e) { - return occurs(mk_placholder(), e); + return occurs(mk_placeholder(), e); } class replace_placeholders_with_metavars_proc : public replace_visitor { diff --git a/src/library/placeholder.h b/src/library/placeholder.h index 7e2e936fa..6d0939e4b 100644 --- a/src/library/placeholder.h +++ b/src/library/placeholder.h @@ -14,7 +14,7 @@ class metavar_env; \brief Return a new placeholder expression. To be able to track location, a new constant for each placeholder. */ -expr mk_placholder(); +expr mk_placeholder(); /** \brief Return true iff the given expression is a placeholder. diff --git a/src/tests/kernel/metavar.cpp b/src/tests/kernel/metavar.cpp index 49beab810..06ad8a67c 100644 --- a/src/tests/kernel/metavar.cpp +++ b/src/tests/kernel/metavar.cpp @@ -446,7 +446,7 @@ static void tst21() { add_lift(m1, 1, 7)); } -#define _ mk_placholder() +#define _ mk_placeholder() static void tst22() { metavar_env menv; diff --git a/src/tests/library/elaborator/elaborator.cpp b/src/tests/library/elaborator/elaborator.cpp index 899c29d52..b066c19e3 100644 --- a/src/tests/library/elaborator/elaborator.cpp +++ b/src/tests/library/elaborator/elaborator.cpp @@ -266,7 +266,7 @@ static void tst6() { std::cout << instantiate_metavars(V, s) << "\n"; } -#define _ mk_placholder() +#define _ mk_placeholder() static expr elaborate(expr const & e, environment const & env) { metavar_env menv;