From 443022d84027331a472c5bd8524f885b55189f6d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 26 Jun 2014 18:51:35 -0700 Subject: [PATCH] feat(util/lazy_list): add is_nil predicate Signed-off-by: Leonardo de Moura --- src/util/lazy_list.h | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/src/util/lazy_list.h b/src/util/lazy_list.h index d13629e50..9511d734f 100644 --- a/src/util/lazy_list.h +++ b/src/util/lazy_list.h @@ -73,6 +73,26 @@ public: lazy_list & operator=(lazy_list const & s) { LEAN_COPY_REF(s); } lazy_list & operator=(lazy_list && s) { LEAN_MOVE_REF(s); } + /** + \brief Return true if the lazy_list is definitely empty. This is an approximated test (i.e., it is not an "iff"). + Here are examples where this method will return true. + + 1) lazy_list empty; + lean_assert(is_nil(empty)); + + 2) lazy_list singleton(v); + maybe_pair p = singleton.pull(); + lean_assert(p); + lean_assert(is_nil(p->second)); + + 3) assume is_nil(l), then + lazy_list singleton(v, l); + maybe_pair p = singleton.pull(); + lean_assert(p); + lean_assert(is_nil(p->second)); + */ + bool is_nil() const { return m_ptr == nullptr; } + maybe_pair pull() const { if (m_ptr) return m_ptr->pull();