From 802edd77d17c0c5317a4bd1b92cfa3e02b4c8d50 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 2 May 2014 12:15:29 -0700 Subject: [PATCH] feat(kernel/justification): add is_eqp predicate Signed-off-by: Leonardo de Moura --- src/kernel/justification.h | 2 ++ src/library/kernel_bindings.cpp | 2 ++ 2 files changed, 4 insertions(+) diff --git a/src/kernel/justification.h b/src/kernel/justification.h index 8a6b0d8ee..66216245a 100644 --- a/src/kernel/justification.h +++ b/src/kernel/justification.h @@ -72,6 +72,8 @@ public: friend justification mk_assumption_justification(unsigned idx, optional const & s, pp_jst_fn const & fn); friend justification mk_assumption_justification(unsigned idx); friend justification mk_justification(optional const & s, pp_jst_fn const & fn); + + friend bool is_eqp(justification const & j1, justification const & j2) { return j1.raw() == j2.raw(); } }; /** diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp index 15467aa89..4f2aac117 100644 --- a/src/library/kernel_bindings.cpp +++ b/src/library/kernel_bindings.cpp @@ -958,6 +958,7 @@ static int mk_justification(lua_State * L) { return push_justification(L, j); } } +static int justification_is_eqp(lua_State * L) { return push_boolean(L, is_eqp(to_justification(L, 1), to_justification(L, 2))); } static const struct luaL_Reg justification_m[] = { {"__gc", justification_gc}, // never throws @@ -972,6 +973,7 @@ static const struct luaL_Reg justification_m[] = { {"assumption_idx", safe_function}, {"child1", safe_function}, {"child2", safe_function}, + {"is_eqp", safe_function}, {0, 0} };