From f9a21166f02e4a7f03b2e2f46e9279de9da0158e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 21 Jun 2014 19:45:20 -0700
Subject: [PATCH] feat(kernel/type_checker): add type_checker::is_def_eq method
 that takes a justification as argument

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/kernel/justification.h  | 7 +++++++
 src/kernel/type_checker.cpp | 5 +++++
 src/kernel/type_checker.h   | 1 +
 3 files changed, 13 insertions(+)

diff --git a/src/kernel/justification.h b/src/kernel/justification.h
index 608ce38f1..3b80385e1 100644
--- a/src/kernel/justification.h
+++ b/src/kernel/justification.h
@@ -161,4 +161,11 @@ public:
     template<typename Mk> simple_delayed_justification(Mk && mk):m_mk(mk) {}
     virtual justification get() { if (!m_jst) { m_jst = m_mk(); } return *m_jst; }
 };
+
+class as_delayed_justification : public delayed_justification {
+    justification m_jst;
+public:
+    as_delayed_justification(justification const & j):m_jst(j) {}
+    virtual justification get() { return m_jst; }
+};
 }
diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index 20032199c..5380da01c 100644
--- a/src/kernel/type_checker.cpp
+++ b/src/kernel/type_checker.cpp
@@ -400,6 +400,10 @@ struct type_checker::imp {
         return infer_type_core(e, false);
     }
     bool is_def_eq(expr const & t, expr const & s) { return m_conv->is_def_eq(t, s, m_conv_ctx); }
+    bool is_def_eq(expr const & t, expr const & s, justification const & j) {
+        as_delayed_justification djst(j);
+        return is_def_eq(t, s, djst);
+    }
     expr whnf(expr const & t) { return m_conv->whnf(t, m_conv_ctx); }
 };
 
@@ -421,6 +425,7 @@ type_checker::~type_checker() {}
 expr type_checker::infer(expr const & t) { return m_ptr->infer_type(t); }
 expr type_checker::check(expr const & t, level_param_names const & ps) { return m_ptr->check(t, ps); }
 bool type_checker::is_def_eq(expr const & t, expr const & s) { return m_ptr->is_def_eq(t, s); }
+bool type_checker::is_def_eq(expr const & t, expr const & s, justification const & j) { return m_ptr->is_def_eq(t, s, j); }
 bool type_checker::is_prop(expr const & t) { return m_ptr->is_prop(t); }
 expr type_checker::whnf(expr const & t) { return m_ptr->whnf(t); }
 expr type_checker::ensure_pi(expr const & t, expr const & s) { return m_ptr->ensure_pi(t, s); }
diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h
index 1c1d22534..54f1f0d9b 100644
--- a/src/kernel/type_checker.h
+++ b/src/kernel/type_checker.h
@@ -81,6 +81,7 @@ public:
     expr check(expr const & t, level_param_names const & ps = level_param_names());
     /** \brief Return true iff t is definitionally equal to s. */
     bool is_def_eq(expr const & t, expr const & s);
+    bool is_def_eq(expr const & t, expr const & s, justification const & j);
     /** \brief Return true iff t is a proposition. */
     bool is_prop(expr const & t);
     /** \brief Return the weak head normal form of \c t. */