feat(kernel/justification): add is_eqp predicate

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/kernel/justification.h

@@ -72,6 +72,8 @@ public:
     friend justification mk_assumption_justification(unsigned idx, optional<expr> const & s, pp_jst_fn const & fn);
     friend justification mk_assumption_justification(unsigned idx);
     friend justification mk_justification(optional<expr> const & s, pp_jst_fn const & fn);
+
+    friend bool is_eqp(justification const & j1, justification const & j2) { return j1.raw() == j2.raw(); }
 };
 
 /**

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<justification_assumption_idx>},
     {"child1",          safe_function<justification_child1>},
     {"child2",          safe_function<justification_child2>},
+    {"is_eqp",          safe_function<justification_is_eqp>},
     {0, 0}
 };