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

fix(frontends/lean/elaborator): ignore mdata when processing field notation

Browse source
This commit is contained in:
Leonardo de Moura 2019-02-11 17:29:38 -08:00
parent e920faf76d
commit 9675b7c952
3 changed files with 11 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -1903,7 +1903,7 @@ expr elaborator::visit_app_core(expr fn, buffer<expr> const & args, optional<exp
unsigned i = 0;
while (is_pi(proj_type)) {
if (is_explicit(binding_info(proj_type))) {
if (is_app_of(binding_domain(proj_type), field_res.m_base_S_name)) {
if (is_app_of(extract_mdata(binding_domain(proj_type)), field_res.m_base_S_name)) {
/* found s location */
expr coerced_s = *mk_base_projections(m_env, field_res.m_S_name, field_res.m_base_S_name, mk_as_is(s));
new_args.push_back(copy_pos(fn, std::move(coerced_s)));

8
src/library/util.cpp
View file

@ -1030,6 +1030,14 @@ expr mk_tactic_unit() {
static std::string * g_version_string = nullptr;
std::string const & get_version_string() { return *g_version_string; }
expr const & extract_mdata(expr const & e) {
if (is_mdata(e)) {
return extract_mdata(mdata_expr(e));
} else {
return e;
}
}
void initialize_library_util() {
g_unit = new expr(mk_constant(get_unit_name()));
g_unit_mk = new expr(mk_constant(get_unit_star_name()));

2
src/library/util.h
View file

@ -315,6 +315,8 @@ expr mk_tactic_unit();
std::string const & get_version_string();
expr const & extract_mdata(expr const &);
void initialize_library_util();
void finalize_library_util();
}