From a4c2b0303efa1ec0015694a4f306664d650072e2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 9 Jan 2020 16:12:42 -0800
Subject: [PATCH] chore: update stage0

---
 stage0/src/kernel/expr.h           |  2 +-
 stage0/src/kernel/type_checker.cpp | 14 +++++++-------
 stage0/src/util/nat.h              |  2 +-
 3 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/stage0/src/kernel/expr.h b/stage0/src/kernel/expr.h
index f301e551fa..8123b00556 100644
--- a/stage0/src/kernel/expr.h
+++ b/stage0/src/kernel/expr.h
@@ -60,9 +60,9 @@ public:
     literal_kind kind() const { return kind(raw()); }
     string_ref const & get_string() const { lean_assert(kind() == literal_kind::String); return static_cast<string_ref const &>(cnstr_get_ref(*this, 0)); }
     nat const & get_nat() const { lean_assert(kind() == literal_kind::Nat); return static_cast<nat const &>(cnstr_get_ref(*this, 0)); }
+    bool is_zero() const { return kind() == literal_kind::Nat && get_nat().is_zero(); }
     friend bool operator==(literal const & a, literal const & b);
     friend bool operator<(literal const & a, literal const & b);
-
     void serialize(serializer & s) const { s.write_object(raw()); }
     static literal deserialize(deserializer & d) { return literal(d.read_object(), true); }
 };
diff --git a/stage0/src/kernel/type_checker.cpp b/stage0/src/kernel/type_checker.cpp
index 5782c6e7ad..739c5401b2 100644
--- a/stage0/src/kernel/type_checker.cpp
+++ b/stage0/src/kernel/type_checker.cpp
@@ -783,14 +783,14 @@ lbool type_checker::lazy_delta_reduction(expr & t_n, expr & s_n) {
     }
 }
 
-inline bool is_zero(expr const & t) {
-    return t == *g_nat_zero || (is_nat_lit(t) && lit_value(t).get_nat() == nat(0));
+inline bool is_nat_zero(expr const & t) {
+    return t == *g_nat_zero || (is_nat_lit(t) && lit_value(t).is_zero());
 }
 
-inline optional<expr> is_succ(expr const & t) {
+inline optional<expr> is_nat_succ(expr const & t) {
     if (is_nat_lit(t)) {
         nat val = lit_value(t).get_nat();
-        if (val > nat(0)) {
+        if (!val.is_zero()) {
             return some_expr(mk_lit(literal(val - nat(1))));
         }
     }
@@ -802,10 +802,10 @@ inline optional<expr> is_succ(expr const & t) {
 }
 
 lbool type_checker::is_def_eq_offset(expr const & t, expr const & s) {
-    if (is_zero(t) && is_zero(s))
+    if (is_nat_zero(t) && is_nat_zero(s))
         return l_true;
-    optional<expr> pred_t = is_succ(t);
-    optional<expr> pred_s = is_succ(s);
+    optional<expr> pred_t = is_nat_succ(t);
+    optional<expr> pred_s = is_nat_succ(s);
     if (pred_t && pred_s)
         return to_lbool(is_def_eq_core(*pred_t, *pred_s));
     /* TODO add support for Nat.add */
diff --git a/stage0/src/util/nat.h b/stage0/src/util/nat.h
index 28ca4f5a09..8c4c3fd7de 100644
--- a/stage0/src/util/nat.h
+++ b/stage0/src/util/nat.h
@@ -32,9 +32,9 @@ public:
 
     nat & operator=(nat const & other) { object_ref::operator=(other); return *this; }
     nat & operator=(nat && other) { object_ref::operator=(other); return *this; }
-
     bool is_small() const { return is_scalar(raw()); }
     size_t get_small_value() const { lean_assert(is_small()); return unbox(raw()); }
+    bool is_zero() const { return is_small() && get_small_value() == 0; }
     mpz const & get_big_value() const { lean_assert(!is_small()); return mpz_value(raw()); }
     mpz to_mpz() const { return is_small() ? mpz(mpz::of_size_t(unbox(raw()))) : mpz_value(raw()); }
     std::string to_std_string() const { return to_mpz().to_string(); }