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

fix(frontends/lean/inductive_cmds): set m_explicit_levels, and call collect_implicit_locals only after that

Browse source
This commit is contained in:
Sebastian Ullrich 2019-01-15 16:47:28 +01:00
parent 7dd21df59f
commit cead81fcea
3 changed files with 8 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/frontends/lean/inductive_cmds.cpp
View file

@ -777,11 +777,17 @@ environment inductive_cmd(parser & p, cmd_meta const & meta) {
void elaborate_inductive_decls(parser & p, cmd_meta const & meta, buffer<decl_attributes> mut_attrs, buffer<name> lp_names,
name_map<implicit_infer_kind> implicit_infer_map,
buffer<expr> const & params, buffer<expr> const & inds, buffer<buffer<expr> > const & intro_rules) {
buffer<expr> params, buffer<expr> const & inds, buffer<buffer<expr> > const & intro_rules) {
inductive_cmd_fn fn(p, meta);
fn.m_mut_attrs = mut_attrs;
fn.m_lp_names = lp_names;
fn.m_explicit_levels = lp_names.size() || fn.has_explicit_level(intro_rules);
fn.m_implicit_infer_map = implicit_infer_map;
buffer<expr> all_inds_intro_rules;
all_inds_intro_rules.append(inds);
for (buffer<expr> const & irs : intro_rules)
all_inds_intro_rules.append(irs);
collect_implicit_locals(p, fn.m_lp_names, params, all_inds_intro_rules);
inductive_cmd_fn::parse_result r;
fn.elaborate_inductive_decls(params, inds, intro_rules, r.m_params, r.m_inds, r.m_intro_rules);
fn.add_inductive_decls(r);

2
src/frontends/lean/inductive_cmds.h
View file

@ -14,7 +14,7 @@ environment inductive_cmd(parser & p, cmd_meta const & meta);
void elaborate_inductive_decls(parser & p, cmd_meta const & meta, buffer<decl_attributes> mut_attrs, buffer<name> lp_names,
name_map<implicit_infer_kind> implicit_infer_map,
buffer<expr> const & params, buffer<expr> const & inds, buffer<buffer<expr> > const & intro_rules);
buffer<expr> params, buffer<expr> const & inds, buffer<buffer<expr> > const & intro_rules);
void register_inductive_cmds(cmd_table & r);
void initialize_inductive_cmds();

6
src/frontends/lean/vm_elaborator.cpp
View file

@ -288,12 +288,6 @@ static void elab_inductives_cmd(parser & p, expr const & cmd) {
}
}
buffer<expr> all_inds_intro_rules;
all_inds_intro_rules.append(inds);
for (buffer<expr> const & irs : intro_rules)
all_inds_intro_rules.append(irs);
collect_implicit_locals(p, lp_names, params, all_inds_intro_rules);
elaborate_inductive_decls(p, meta, mut_attrs, lp_names, implicit_infer_map, params, inds, intro_rules);
}