diff --git a/library/init/lean/expr.lean b/library/init/lean/expr.lean
index 340f4b136d..77488a96e4 100644
--- a/library/init/lean/expr.lean
+++ b/library/init/lean/expr.lean
@@ -78,9 +78,22 @@ mkApp (Expr.const fn []) args
 @[extern "lean_expr_hash"]
 constant hash (n : @& Expr) : USize := default USize
 
+instance : Hashable Expr := ⟨Expr.hash⟩
+
 @[extern "lean_expr_dbg_to_string"]
 constant dbgToString (e : @& Expr) : String := default String
 
+@[extern "lean_expr_quick_lt"]
+constant quickLt (a : @& Expr) (b : @& Expr) : Bool := default _
+
+@[extern "lean_expr_lt"]
+constant lt (a : @& Expr) (b : @& Expr) : Bool := default _
+
+@[extern "lean_expr_eqv"]
+constant eqv (a : @& Expr) (b : @& Expr) : Bool := default _
+
+instance : HasBeq Expr := ⟨Expr.eqv⟩
+
 end Expr
 
 def getAppFn : Expr → Expr
diff --git a/src/kernel/expr_eq_fn.cpp b/src/kernel/expr_eq_fn.cpp
index 28accbf684..fe47e40a51 100644
--- a/src/kernel/expr_eq_fn.cpp
+++ b/src/kernel/expr_eq_fn.cpp
@@ -133,4 +133,8 @@ bool is_equal(expr const & a, expr const & b) {
 bool is_bi_equal(expr const & a, expr const & b) {
     return expr_eq_fn<true>()(a, b);
 }
+
+extern "C" uint8 lean_expr_eqv(b_obj_arg a, b_obj_arg b) {
+    return expr_eq_fn<false>()(expr(a, true), expr(b, true));
+}
 }
diff --git a/src/library/expr_lt.cpp b/src/library/expr_lt.cpp
index e60315807f..5214d6d968 100644
--- a/src/library/expr_lt.cpp
+++ b/src/library/expr_lt.cpp
@@ -202,4 +202,12 @@ int expr_cmp_no_level_params::operator()(expr const & e1, expr const & e2) const
     else
         return 0;
 }
+
+extern "C" uint8 lean_expr_quick_lt(b_obj_arg a, b_obj_arg b) {
+    return is_lt(expr(a, true), expr(b, true), true, nullptr);
+}
+
+extern "C" uint8 lean_expr_lt(b_obj_arg a, b_obj_arg b) {
+    return is_lt(expr(a, true), expr(b, true), false, nullptr);
+}
 }
diff --git a/src/stage0/init/lean/expr.cpp b/src/stage0/init/lean/expr.cpp
index 490e129916..ad97f392cc 100644
--- a/src/stage0/init/lean/expr.cpp
+++ b/src/stage0/init/lean/expr.cpp
@@ -15,6 +15,7 @@ typedef lean::uint32 uint32; typedef lean::uint64 uint64;
 #pragma GCC diagnostic ignored "-Wunused-but-set-variable"
 #endif
 obj* l_Lean_getAppFn___main(obj*);
+extern "C" uint8 lean_expr_quick_lt(obj*, obj*);
 obj* l_Lean_Expr_hash___boxed(obj*);
 obj* l_Lean_mkBinApp(obj*, obj*, obj*);
 obj* l_Lean_MData_empty;
@@ -23,10 +24,13 @@ obj* l_Lean_exprIsInhabited;
 extern "C" usize lean_expr_hash(obj*);
 obj* l_Lean_getAppFn___main___boxed(obj*);
 extern "C" obj* lean_expr_dbg_to_string(obj*);
+obj* l_Lean_Expr_eqv___boxed(obj*, obj*);
 extern "C" obj* lean_expr_mk_app(obj*, obj*);
+obj* l_Lean_Expr_quickLt___boxed(obj*, obj*);
 obj* l_Lean_Expr_mkCapp(obj*, obj*);
 obj* l_Lean_mkDecIsFalse___closed__1;
 extern "C" obj* lean_expr_mk_const(obj*, obj*);
+extern "C" uint8 lean_expr_eqv(obj*, obj*);
 obj* l_List_foldl___main___at_Lean_Expr_mkApp___spec__1(obj*, obj*);
 obj* l_Lean_MData_HasEmptyc;
 obj* l_Lean_Expr_dbgToString___boxed(obj*);
@@ -34,8 +38,12 @@ obj* l_Lean_mkDecIsTrue___closed__1;
 obj* l_Lean_mkDecIsFalse(obj*, obj*);
 extern "C" obj* lean_name_mk_string(obj*, obj*);
 obj* l_Lean_getAppFn___boxed(obj*);
+extern "C" uint8 lean_expr_lt(obj*, obj*);
 obj* l_Lean_mkDecIsTrue(obj*, obj*);
+obj* l_Lean_Expr_HasBeq;
 obj* l_Lean_Expr_mkApp(obj*, obj*);
+obj* l_Lean_Expr_Hashable;
+obj* l_Lean_Expr_lt___boxed(obj*, obj*);
 obj* _init_l_Lean_MData_empty() {
 _start:
 {
@@ -112,6 +120,14 @@ lean::dec(x_0);
 return x_2;
 }
 }
+obj* _init_l_Lean_Expr_Hashable() {
+_start:
+{
+obj* x_0; 
+x_0 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Expr_hash___boxed), 1, 0);
+return x_0;
+}
+}
 obj* l_Lean_Expr_dbgToString___boxed(obj* x_0) {
 _start:
 {
@@ -121,6 +137,47 @@ lean::dec(x_0);
 return x_1;
 }
 }
+obj* l_Lean_Expr_quickLt___boxed(obj* x_0, obj* x_1) {
+_start:
+{
+uint8 x_2; obj* x_3; 
+x_2 = lean_expr_quick_lt(x_0, x_1);
+x_3 = lean::box(x_2);
+lean::dec(x_0);
+lean::dec(x_1);
+return x_3;
+}
+}
+obj* l_Lean_Expr_lt___boxed(obj* x_0, obj* x_1) {
+_start:
+{
+uint8 x_2; obj* x_3; 
+x_2 = lean_expr_lt(x_0, x_1);
+x_3 = lean::box(x_2);
+lean::dec(x_0);
+lean::dec(x_1);
+return x_3;
+}
+}
+obj* l_Lean_Expr_eqv___boxed(obj* x_0, obj* x_1) {
+_start:
+{
+uint8 x_2; obj* x_3; 
+x_2 = lean_expr_eqv(x_0, x_1);
+x_3 = lean::box(x_2);
+lean::dec(x_0);
+lean::dec(x_1);
+return x_3;
+}
+}
+obj* _init_l_Lean_Expr_HasBeq() {
+_start:
+{
+obj* x_0; 
+x_0 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_Expr_eqv___boxed), 2, 0);
+return x_0;
+}
+}
 obj* l_Lean_getAppFn___main(obj* x_0) {
 _start:
 {
@@ -238,6 +295,10 @@ lean::mark_persistent(l_Lean_MData_empty);
 lean::mark_persistent(l_Lean_MData_HasEmptyc);
  l_Lean_exprIsInhabited = _init_l_Lean_exprIsInhabited();
 lean::mark_persistent(l_Lean_exprIsInhabited);
+ l_Lean_Expr_Hashable = _init_l_Lean_Expr_Hashable();
+lean::mark_persistent(l_Lean_Expr_Hashable);
+ l_Lean_Expr_HasBeq = _init_l_Lean_Expr_HasBeq();
+lean::mark_persistent(l_Lean_Expr_HasBeq);
  l_Lean_mkDecIsTrue___closed__1 = _init_l_Lean_mkDecIsTrue___closed__1();
 lean::mark_persistent(l_Lean_mkDecIsTrue___closed__1);
  l_Lean_mkDecIsFalse___closed__1 = _init_l_Lean_mkDecIsFalse___closed__1();