From d445857f562b271a61acc8739b143c80d5ea0d30 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 8 Oct 2014 19:00:16 -0700 Subject: [PATCH] fix(frontends/lean): change how "as-is" expressions are handled Implicit arguments are consumed. --- src/frontends/lean/elaborator.cpp | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index e1d0384ea..e378b4cfc 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -556,10 +556,14 @@ expr elaborator::visit_sort(expr const & e) { } expr elaborator::visit_macro(expr const & e, constraint_seq & cs) { - 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()); + if (is_as_is(e)) { + return get_as_is_arg(e); + } else { + 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) { @@ -760,9 +764,7 @@ pair elaborator::visit(expr const & e) { expr r; expr b = e; constraint_seq cs; - if (is_as_is(e)) { - r = get_as_is_arg(e); - } else if (is_explicit(e)) { + if (is_explicit(e)) { b = get_explicit_arg(e); if (is_sorry(b)) { r = visit_constant(b);