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

chore(kernel/level): remove unnecessary code

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-02 15:42:37 -07:00
parent 712c10f818
commit 96f639811c
1 changed files with 0 additions and 37 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

37
src/kernel/level.h
View file

@ -218,42 +218,5 @@ format pp(level const & l, options const & opts = options());
format pp(level const & lhs, level const & rhs, bool unicode, unsigned indent); format pp(level const & lhs, level const & rhs, bool unicode, unsigned indent);
/** \brief Pretty print lhs <= rhs using the given configuration options. */ /** \brief Pretty print lhs <= rhs using the given configuration options. */
format pp(level const & lhs, level const & rhs, options const & opts = options()); format pp(level const & lhs, level const & rhs, options const & opts = options());
/** \brief Auxiliary class used to manage universe constraints. */
class universe_context {
struct imp;
std::unique_ptr<imp> m_ptr;
public:
universe_context();
universe_context(universe_context const & s);
~universe_context();
/**
\brief Add the universe level constraint l1 <= l2.
*/
void add_le(level const & l1, level const & l2);
/**
\brief Quick check wether l1 <= l2. No backtracking search is performed.
If the result is true, then l1 <= l2 is implied. The result is false,
if we could not establish that.
*/
bool is_implied_cheap(level const & l1, level const & l2) const;
/**
\brief Expensive l1 <= l2 test. It performs a backtracking search.
*/
bool is_implied(level const & l1, level const & l2);
/**
\brief Create a backtracking point.
*/
void push();
/**
\brief Backtrack.
*/
void pop(unsigned num_scopes);
};
} }
void print(lean::level const & l); void print(lean::level const & l);