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

refactor(library/tactic/goal): remove unnecessary parameter

Browse source
This commit is contained in:
Leonardo de Moura 2014-10-23 21:22:52 -07:00
parent ab4c292872
commit f9aa1a1b84
2 changed files with 4 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/library/tactic/goal.cpp
View file

@ -49,14 +49,9 @@ expr goal::abstract(expr const & v) const {
return Fun(locals, v);
}
expr goal::mk_meta(name const & n, expr const & type, bool only_contextual) const {
expr goal::mk_meta(name const & n, expr const & type) const {
buffer<expr> locals;
expr this_mvar = get_app_args(m_meta, locals);
if (only_contextual) {
auto new_end = std::remove_if(locals.begin(), locals.end(),
[](expr const & l) { return !local_info(l).is_contextual(); });
locals.shrink(locals.size() - (locals.end() - new_end));
}
expr mvar = copy_tag(this_mvar, mk_metavar(n, Pi(locals, type)));
return copy_tag(m_meta, mk_app(mvar, locals));
}
@ -120,8 +115,7 @@ static int goal_tostring(lua_State * L) {
return 1;
}
static int goal_mk_meta(lua_State * L) {
int nargs = lua_gettop(L);
return push_expr(L, to_goal(L, 1).mk_meta(to_name_ext(L, 2), to_expr(L, 3), nargs == 4 ? lua_toboolean(L, 4) : true));
return push_expr(L, to_goal(L, 1).mk_meta(to_name_ext(L, 2), to_expr(L, 3)));
}
static int goal_pp(lua_State * L) {

5
src/library/tactic/goal.h
View file

@ -50,10 +50,9 @@ public:
expr abstract(expr const & v) const;
/** \brief Create a metavariable application <tt>(?m l_1 ... l_n)</tt> with the given type,
and the locals from this goal. If <tt>only_contextual == true</tt>, then we only include
the local constants that are marked as contextual.
and the locals from this goal.
*/
expr mk_meta(name const & m, expr const & type, bool only_contextual = true) const;
expr mk_meta(name const & m, expr const & type) const;
/** \brief Return true iff get_type() only contains local constants that arguments
of get_meta(), and each argument of get_meta() only contains local constants