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

chore(kernel/metavar): remove unused function

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-12 17:39:14 -08:00
parent 450d6a4b1e
commit ae52c8062e
2 changed files with 0 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/kernel/metavar.cpp
View file

@ -51,13 +51,6 @@ public:
virtual optional<expr> get_main_expr() const { return some_expr(m_expr); } virtual optional<expr> get_main_expr() const { return some_expr(m_expr); }
}; };
void swap(metavar_env & a, metavar_env & b) {
swap(a.m_name_generator, b.m_name_generator);
swap(a.m_metavar_data, b.m_metavar_data);
std::swap(a.m_beta_reduce_mv, b.m_beta_reduce_mv);
std::swap(a.m_timestamp, b.m_timestamp);
}
void metavar_env::inc_timestamp() { void metavar_env::inc_timestamp() {
if (m_timestamp == std::numeric_limits<unsigned>::max()) { if (m_timestamp == std::numeric_limits<unsigned>::max()) {
// This should not happen in real examples. We add it just to be safe. // This should not happen in real examples. We add it just to be safe.

2
src/kernel/metavar.h
View file

@ -154,8 +154,6 @@ public:
} }
}; };
void swap(metavar_env & a, metavar_env & b);
/** /**
\brief Apply the changes in \c lctx to \c a. \brief Apply the changes in \c lctx to \c a.
*/ */