From 16041e4948044700907cb051069aca5971e9f5db Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 7 Oct 2014 15:15:50 -0700 Subject: [PATCH] fix(frontends/lean/elaborator): 'as-is' expressions The elaborator should not introduce implicit arguments on terms marked as 'as-is'. --- src/frontends/lean/elaborator.cpp | 18 +++++++----------- 1 file changed, 7 insertions(+), 11 deletions(-) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 9fa662de5..323d54a29 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -556,16 +556,10 @@ expr elaborator::visit_sort(expr const & e) { } expr elaborator::visit_macro(expr const & e, constraint_seq & cs) { - if (is_as_is(e)) { - return get_as_is_arg(e); - } else { - // Remark: Macros are not meant to be used in the front end. - // Perhaps, we should throw error. - buffer args; - for (unsigned i = 0; i < macro_num_args(e); i++) - args.push_back(visit(macro_arg(e, i), cs)); - return update_macro(e, args.size(), args.data()); - } + buffer args; + for (unsigned i = 0; i < macro_num_args(e); i++) + args.push_back(visit(macro_arg(e, i), cs)); + return update_macro(e, args.size(), args.data()); } expr elaborator::visit_constant(expr const & e) { @@ -766,7 +760,9 @@ pair elaborator::visit(expr const & e) { expr r; expr b = e; constraint_seq cs; - if (is_explicit(e)) { + if (is_as_is(e)) { + r = get_as_is_arg(e); + } else if (is_explicit(e)) { b = get_explicit_arg(e); if (is_sorry(b)) { r = visit_constant(b);