From 16d7ee5aff6bbf3f3fd258fb9236ba3b8967554c Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 17 Jan 2019 14:37:13 +0100 Subject: [PATCH] fix(frontends/lean/vm_elaborator): pattern variables --- src/frontends/lean/vm_elaborator.cpp | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/src/frontends/lean/vm_elaborator.cpp b/src/frontends/lean/vm_elaborator.cpp index 74e1943f89..e8e44bb981 100644 --- a/src/frontends/lean/vm_elaborator.cpp +++ b/src/frontends/lean/vm_elaborator.cpp @@ -84,11 +84,16 @@ struct resolve_names_fn : public replace_visitor { flet _(m_assume_local, true); lhs = visit(lhs); } - buffer locals; + buffer new_locals; bool skip_main_fn = true; - lhs = m_p.patexpr_to_pattern(lhs, skip_main_fn, locals); + lhs = m_p.patexpr_to_pattern(lhs, skip_main_fn, new_locals); + names locals; + // NOTE: appends `new_locals` to `locals` in reverse + for (auto const & l : new_locals) + locals = cons(local_name_p(l), locals); + flet _(m_locals, locals); rhs = visit(rhs); - eqn = Fun(locals, mk_equation(lhs, rhs), m_p); + eqn = Fun(new_locals, mk_equation(lhs, rhs), m_p); } } return mk_equations(header, eqns.size(), eqns.data()); @@ -241,6 +246,7 @@ static expr unpack_mutual_definition(parser & p, expr const & cmd, buffer full_actual_names.push_back(scope3.get_actual_name()); prv_names.push_back(scope2.get_actual_name()); fn = mk_local(n, n, fn_type, mk_rec_info()); + p.add_local(fn); } optional wf_tacs; if (args.size() > 6)