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

chore(frontends/lean/frontend): remove dead code

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-07 15:28:21 -08:00
parent 9f4959fb64
commit a3af87f8d3
2 changed files with 0 additions and 26 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
src/frontends/lean/frontend.cpp
View file

@ -635,29 +635,9 @@ optional<unsigned> get_lbp(ro_environment const & env, name const & n) {
void mark_implicit_arguments(environment const & env, name const & n, unsigned sz, bool const * implicit) {
to_ext(env).mark_implicit_arguments(n, sz, implicit, env);
}
void mark_implicit_arguments(environment const & env, name const & n, unsigned prefix_sz) {
buffer<bool> implicit; implicit.resize(prefix_sz, true);
mark_implicit_arguments(env, n, implicit.size(), implicit.data());
}
void mark_implicit_arguments(environment const & env, expr const & n, unsigned prefix_sz) {
if (is_constant(n)) {
mark_implicit_arguments(env, const_name(n), prefix_sz);
} else {
lean_assert(is_value(n));
mark_implicit_arguments(env, to_value(n).get_name(), prefix_sz);
}
}
void mark_implicit_arguments(environment const & env, name const & n, std::initializer_list<bool> const & l) {
mark_implicit_arguments(env, n, l.size(), l.begin());
}
void mark_implicit_arguments(environment const & env, expr const & n, std::initializer_list<bool> const & l) {
if (is_constant(n)) {
mark_implicit_arguments(env, const_name(n), l);
} else {
lean_assert(is_value(n));
mark_implicit_arguments(env, to_value(n).get_name(), l);
}
}
bool has_implicit_arguments(ro_environment const & env, name const & n) {
return to_ext(env).has_implicit_arguments(n);
}

6
src/frontends/lean/frontend.h
View file

@ -98,12 +98,6 @@ operator_info find_op_for(ro_environment const & env, expr const & e, bool unico
*/
void mark_implicit_arguments(environment const & env, name const & n, unsigned sz, bool const * implicit);
void mark_implicit_arguments(environment const & env, name const & n, std::initializer_list<bool> const & l);
void mark_implicit_arguments(environment const & env, expr const & n, std::initializer_list<bool> const & l);
/**
\brief Syntax sugar for mark_implicit_arguments(n, {true, ..., true}), with prefix_sz true's.
*/
void mark_implicit_arguments(environment const & env, name const & n, unsigned prefix_sz);
void mark_implicit_arguments(environment const & env, expr const & n, unsigned prefix_sz);
/**
\brief Return true iff \c n has implicit arguments
*/