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

feat(library/expr_lt): add lex comparison for expression pairs

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-06-17 12:14:22 -07:00
parent 28c904abea
commit f9d81c24d3
1 changed files with 7 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/library/expr_pair.h
View file

@ -8,6 +8,7 @@ Author: Leonardo de Moura
#include <utility> #include <utility>
#include "util/hash.h" #include "util/hash.h"
#include "kernel/expr.h" #include "kernel/expr.h"
#include "library/expr_lt.h"
namespace lean { namespace lean {
typedef std::pair<expr, expr> expr_pair; typedef std::pair<expr, expr> expr_pair;
@ -27,4 +28,10 @@ struct expr_pair_eq {
struct expr_pair_eqp { struct expr_pair_eqp {
unsigned operator()(expr_pair const & p1, expr_pair const & p2) const { return is_eqp(p1.first, p2.first) && is_eqp(p1.second, p2.second); } unsigned operator()(expr_pair const & p1, expr_pair const & p2) const { return is_eqp(p1.first, p2.first) && is_eqp(p1.second, p2.second); }
}; };
inline bool is_lt(expr_pair const & p1, expr_pair const & p2, bool use_hash) {
return is_lt(p1.first, p2.first, use_hash) || (p1.first == p2.first && is_lt(p1.second, p2.second, use_hash));
}
struct expr_pair_quick_cmp {
int operator()(expr_pair const & p1, expr_pair const & p2) const { return is_lt(p1, p2, true) ? -1 : (p1 == p2 ? 0 : 1); }
};
} }