michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(frontends/lean/util): add auxiliary function

Browse source
This commit is contained in:
Leonardo de Moura 2014-10-10 15:21:08 -07:00
parent a41850227a
commit d61e6fdd89
3 changed files with 5 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -378,7 +378,7 @@ environment definition_cmd_core(parser & p, bool is_theorem, bool is_opaque, boo
levels section_ls = collect_section_nonvar_levels(p, ls);
remove_section_variables(p, section_ps);
if (!section_ps.empty()) {
expr ref = mk_section_local_ref(real_n, section_ls, section_ps.size(), section_ps.data());
expr ref = mk_section_local_ref(real_n, section_ls, section_ps);
p.add_local_expr(n, ref);
} else if (section_ls) {
expr ref = mk_constant(real_n, section_ls);

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

@ -594,7 +594,7 @@ struct inductive_cmd_fn {
else
id = name(full_id.get_string());
if (in_section_or_context(env)) {
expr r = mk_section_local_ref(full_id, section_levels, section_params.size(), section_params.data());
expr r = mk_section_local_ref(full_id, section_levels, section_params);
m_p.add_local_expr(id, r);
}
if (full_id != id)

3
src/frontends/lean/util.h
View file

@ -36,6 +36,9 @@ list<expr> locals_to_context(expr const & e, parser const & p);
That is, when the user writes \c n inside the section she is really getting the term returned by this function.
*/
expr mk_section_local_ref(name const & n, levels const & sec_ls, unsigned num_sec_params, expr const * sec_params);
inline expr mk_section_local_ref(name const & n, levels const & sec_ls, buffer<expr> const & sec_params) {
return mk_section_local_ref(n, sec_ls, sec_params.size(), sec_params.data());
}
/** \brief Return true iff \c e is a term of the form
<tt>(@^-1 (@n.{ls} @l_1 ... @l_n))</tt> where
\c n is a constant and l_i's are local constants.