max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat(frontends/lean/elaborator): erase info annotations

Browse source
This commit is contained in:
Leonardo de Moura 2016-08-02 15:43:23 -07:00
parent 186d82d58d
commit 112aae2928
1 changed files with 9 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/frontends/lean/elaborator.cpp
View file

@ -32,6 +32,7 @@ Author: Leonardo de Moura
#include "library/tactic/elaborate.h"
#include "frontends/lean/prenum.h"
#include "frontends/lean/elaborator.h"
#include "frontends/lean/info_annotation.h"
namespace lean {
MK_THREAD_LOCAL_GET(type_context_cache_helper, get_tch, true /* use binder information at infer_cache */);
@ -1048,6 +1049,14 @@ expr elaborator::visit_macro(expr const & e, optional<expr> const & expected_typ
return visit_app_core(e, buffer<expr>(), expected_type, e);
} else if (is_by(e)) {
return visit_by(e, expected_type);
} else if (is_no_info(e)) {
// TODO(Leo): flet<bool> let(m_no_info, true);
return visit(get_annotation_arg(e), expected_type);
} else if (is_notation_info(e)) {
// flet<bool> let(m_no_info, true);
expr r = visit(get_annotation_arg(e), expected_type);
// save_type_data(e, r);
return r;
} else if (is_rec_fn_macro(e)) {
// TODO(Leo)
lean_unreachable();