diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index 4768eca23c..a34dff6ecb 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -348,8 +348,7 @@ static expr parse_including_expr(parser & p, unsigned, expr const *, pos_info co parser::local_scope scope(p); buffer new_locals; for (auto old_l : locals) { - binder_info bi = local_info(old_l); - bi = bi.update_contextual(true); + binder_info bi = mk_contextual_info(true); expr new_l = p.save_pos(mk_local(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); diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index d579842f9b..b2258ed176 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -202,6 +202,11 @@ static void check_end_of_theorem(parser const & p) { throw parser_error("':=', '.', command, script, or end-of-file expected", p.pos()); } +static void erase_local_binder_info(buffer & ps) { + for (expr & p : ps) + p = update_local(p, binder_info()); +} + environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) { auto n_pos = p.pos(); unsigned start_line = n_pos.first; @@ -260,6 +265,7 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) { value = p.parse_scoped_expr(ps, *lenv); } type = Pi(ps, type, p); + erase_local_binder_info(ps); value = Fun(ps, value, p); } @@ -285,7 +291,10 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool _is_opaque) { buffer section_ps; collect_section_locals(type, value, p, section_ps); type = Pi_as_is(section_ps, type, p); - value = Fun_as_is(section_ps, value, p); + buffer section_value_ps; + section_value_ps.append(section_ps); + erase_local_binder_info(section_value_ps); + value = Fun_as_is(section_value_ps, value, p); levels section_ls = collect_section_levels(ls, p); for (expr & p : section_ps) p = mk_explicit(p); diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 3185b802b4..36c01f9d3b 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -1248,16 +1248,14 @@ public: } else { r = visit_core(e, cs); } - if (!is_lambda(r)) { - tag g = e.get_tag(); - expr r_type = whnf(infer_type(r, cs), cs); - expr imp_arg; - bool is_strict = false; - while (is_pi(r_type) && binding_info(r_type).is_implicit()) { - imp_arg = mk_placeholder_meta(some_expr(binding_domain(r_type)), g, is_strict, cs); - r = mk_app(r, imp_arg, g); - r_type = whnf(instantiate(binding_body(r_type), imp_arg), cs); - } + tag g = e.get_tag(); + expr r_type = whnf(infer_type(r, cs), cs); + expr imp_arg; + bool is_strict = false; + while (is_pi(r_type) && binding_info(r_type).is_implicit()) { + imp_arg = mk_placeholder_meta(some_expr(binding_domain(r_type)), g, is_strict, cs); + r = mk_app(r, imp_arg, g); + r_type = whnf(instantiate(binding_body(r_type), imp_arg), cs); } } save_type_data(b, r); diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp index c63d388066..6c8f1b6e34 100644 --- a/src/kernel/expr.cpp +++ b/src/kernel/expr.cpp @@ -553,6 +553,10 @@ expr update_local(expr const & e, expr const & new_type, binder_info const & bi) return copy_tag(e, mk_local(mlocal_name(e), local_pp_name(e), new_type, bi)); } +expr update_local(expr const & e, binder_info const & bi) { + return update_local(e, mlocal_type(e), bi); +} + expr update_sort(expr const & e, level const & new_level) { if (!is_eqp(sort_level(e), new_level)) return copy_tag(e, mk_sort(new_level)); diff --git a/src/kernel/expr.h b/src/kernel/expr.h index 631d9eeb1d..96014ab3f3 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -676,6 +676,7 @@ expr update_binding(expr const & e, expr const & new_domain, expr const & new_bo expr update_binding(expr const & e, expr const & new_domain, expr const & new_body, binder_info const & bi); expr update_mlocal(expr const & e, expr const & new_type); expr update_local(expr const & e, expr const & new_type, binder_info const & bi); +expr update_local(expr const & e, binder_info const & bi); expr update_sort(expr const & e, level const & new_level); expr update_constant(expr const & e, levels const & new_levels); expr update_macro(expr const & e, unsigned num, expr const * args); diff --git a/tests/lean/pp.lean.expected.out b/tests/lean/pp.lean.expected.out index be3384c8e0..fa9299df1f 100644 --- a/tests/lean/pp.lean.expected.out +++ b/tests/lean/pp.lean.expected.out @@ -1,5 +1,5 @@ -λ {A : Type} (B : Type) (a : A) (b : B), a : Π {A : Type} (B : Type), A → B → A -λ {A B : Type} (a : A) (b : B), a : Π {A B : Type}, A → B → A +λ {A : Type} (B : Type) (a : A) (b : B), a : Π (B : Type), ?M_1 → B → ?M_1 +λ {A B : Type} (a : A) (b : B), a : ?M_1 → ?M_2 → ?M_1 λ (A : Type) {B : Type} (a : A) (b : B), a : Π (A : Type) {B : Type}, A → B → A λ (A B : Type) (a : A) (b : B), a : Π (A B : Type), A → B → A λ [A : Type] (B : Type) (a : A) (b : B), a : Π [A : Type] (B : Type), A → B → A diff --git a/tests/lean/run/imp2.lean b/tests/lean/run/imp2.lean new file mode 100644 index 0000000000..98d384f73f --- /dev/null +++ b/tests/lean/run/imp2.lean @@ -0,0 +1,4 @@ +import data.num +check (λ {A : Type} (a : A), a) 10 +check (λ {A} a, a) 10 +check (λ a, a) 10 diff --git a/tests/lean/t7.lean.expected.out b/tests/lean/t7.lean.expected.out index 308042071f..022fc6d0be 100644 --- a/tests/lean/t7.lean.expected.out +++ b/tests/lean/t7.lean.expected.out @@ -2,5 +2,5 @@ id : ?M_1 → ?M_1 trans : (?M_1 → ?M_1 → Prop) → Prop symm : (?M_1 → ?M_1 → Prop) → Prop equivalence : (?M_1 → ?M_1 → Prop) → Prop -λ {A : Type} (R : A → A → Prop), +λ (A : Type) (R : A → A → Prop), and (and (refl R) (symm R)) (trans R)