From b37b4f3dc8a5ebd1532c5a11f2e7e69ddb2220a9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 28 Aug 2016 07:34:04 -0700 Subject: [PATCH] fix(frontends/lean/elaborator): implicit terms are marked as inaccessible in patterns --- src/frontends/lean/elaborator.cpp | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index c14a03c29b..9f7688fdd4 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -807,6 +807,9 @@ optional elaborator::visit_app_propagate_expected(expr const & fn, buffer< new_arg = mk_instance(d, ref); else new_arg = mk_metavar(d); + // implicit arguments are tagged as inaccessible in patterns + if (m_in_pattern) + new_arg = copy_tag(ref, mk_inaccessible(new_arg)); } else if (i < args.size()) { // explicit argument i++; @@ -908,6 +911,9 @@ expr elaborator::visit_default_app_core(expr const & _fn, arg_mask amask, buffer new_arg = mk_instance(d, ref); else new_arg = mk_metavar(d); + // implicit arguments are tagged as inaccessible in patterns + if (m_in_pattern) + new_arg = copy_tag(ref, mk_inaccessible(new_arg)); } else if (i < args.size()) { // explicit argument expr ref_arg = args[i];