From 7ddc3c72dde7c155c101af64143da59853fc683d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 31 Jul 2016 20:49:53 -0700 Subject: [PATCH] fix(frontends/lean/elaborator, library/vm/vm_qexpr): add and handle as_is annotation --- src/frontends/lean/elaborator.cpp | 4 ++-- src/library/vm/vm_qexpr.cpp | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 7c4d1eb6c3..318cd02e3e 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -1364,8 +1364,8 @@ static expr translate_local_name(environment const & env, local_context const & */ static expr translate(environment const & env, local_context const & lctx, expr const & e) { auto fn = [&](expr const & e) { - if (is_placeholder(e) || is_by(e)) { - return some_expr(e); // ignore placeholders + if (is_placeholder(e) || is_by(e) || is_as_is(e)) { + return some_expr(e); // ignore placeholders, nested tactics and as_is terms } else if (is_constant(e)) { expr new_e = copy_tag(e, translate_local_name(env, lctx, const_name(e), e)); return some_expr(new_e); diff --git a/src/library/vm/vm_qexpr.cpp b/src/library/vm/vm_qexpr.cpp index e2f6ba84fd..f4123c25a0 100644 --- a/src/library/vm/vm_qexpr.cpp +++ b/src/library/vm/vm_qexpr.cpp @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include "kernel/instantiate.h" +#include "library/explicit.h" #include "library/vm/vm.h" #include "library/vm/vm_expr.h" @@ -20,8 +21,7 @@ vm_obj qexpr_subst(vm_obj const & _e1, vm_obj const & _e2) { } vm_obj qexpr_of_expr(vm_obj const & e) { - // TODO(Leo): use "as_is" macro - return e; + return to_obj(mk_as_is(to_expr(e))); } vm_obj expr_to_string(vm_obj const &);