From 275cfeac1a52844e7bb314269e6bcf7bfddf6021 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 8 Dec 2016 12:58:10 -0800
Subject: [PATCH] fix(library/type_context): incorrect assertion

---
 src/library/type_context.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp
index 897f70f5be..4ba9ab1b68 100644
--- a/src/library/type_context.cpp
+++ b/src/library/type_context.cpp
@@ -2566,7 +2566,7 @@ lbool type_context::try_offset_eq_numeral(expr const & t, expr const & s) {
     if (*k2 >= *k1) {
         return to_lbool(is_def_eq_core(get_offset_term(t), to_nat_expr(mpz(*k2 - *k1))));
     } else {
-        lean_assert(*k1 < *k2);
+        lean_assert(*k2 < *k1);
         return l_false;
     }
 }