diff --git a/src/frontends/lean/frontend.cpp b/src/frontends/lean/frontend.cpp index 74d6a23c6..0fd492fdd 100644 --- a/src/frontends/lean/frontend.cpp +++ b/src/frontends/lean/frontend.cpp @@ -403,7 +403,7 @@ operator_info frontend::find_op_for(expr const & n, bool unicode) const { return r; } else { object const & obj = find_object(const_name(n)); - if (obj && obj.is_builtin() && obj.get_name() == n) + if (obj && obj.is_builtin() && obj.get_name() == const_name(n)) return to_ext(m_env).find_op_for(obj.get_value(), unicode); else return r; diff --git a/src/frontends/lean/operator_info.h b/src/frontends/lean/operator_info.h index 686b1dc92..3daef1d30 100644 --- a/src/frontends/lean/operator_info.h +++ b/src/frontends/lean/operator_info.h @@ -46,7 +46,7 @@ public: friend void swap(operator_info & o1, operator_info & o2) { std::swap(o1.m_ptr, o2.m_ptr); } - operator bool() const { return m_ptr != nullptr; } + explicit operator bool() const { return m_ptr != nullptr; } friend operator_info infix(name const & op, unsigned precedence); friend operator_info infixl(name const & op, unsigned precedence); diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index e0ee6b92d..282869e46 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -1121,12 +1121,12 @@ class pp_fn { } bool uses_prefix(expr const & e, name const & prefix) { - return find(e, [&](expr const & e) { - return - (is_constant(e) && is_prefix_of(prefix, const_name(e))) || - (is_abstraction(e) && is_prefix_of(prefix, abst_name(e))) || - (is_let(e) && is_prefix_of(prefix, let_name(e))); - }); + return static_cast(find(e, [&](expr const & e) { + return + (is_constant(e) && is_prefix_of(prefix, const_name(e))) || + (is_abstraction(e) && is_prefix_of(prefix, abst_name(e))) || + (is_let(e) && is_prefix_of(prefix, let_name(e))); + })); } name find_unused_prefix(expr const & e) { diff --git a/src/kernel/context.h b/src/kernel/context.h index 92058bc4b..f9436d926 100644 --- a/src/kernel/context.h +++ b/src/kernel/context.h @@ -39,7 +39,7 @@ public: context_entry const & lookup(unsigned vidx) const; std::pair lookup_ext(unsigned vidx) const; bool empty() const { return is_nil(m_list); } - operator bool() const { return !empty(); } + explicit operator bool() const { return !empty(); } unsigned size() const { return length(m_list); } typedef list::iterator iterator; iterator begin() const { return m_list.begin(); } diff --git a/src/kernel/environment.h b/src/kernel/environment.h index 7ea90b9b9..9a5c1a6e6 100644 --- a/src/kernel/environment.h +++ b/src/kernel/environment.h @@ -148,7 +148,7 @@ public: object const & find_object(name const & n) const; /** \brief Return true iff the environment has an object with the given name */ - bool has_object(name const & n) const { return find_object(n); } + bool has_object(name const & n) const { return static_cast(find_object(n)); } /** \brief Return the type of \c e in the given context and this environment. diff --git a/src/kernel/expr.h b/src/kernel/expr.h index d147efd4a..4fd952b55 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -123,7 +123,7 @@ public: expr_cell * raw() const { return m_ptr; } - operator bool() const { return m_ptr != nullptr; } + explicit operator bool() const { return m_ptr != nullptr; } friend expr mk_var(unsigned idx); friend expr mk_constant(name const & n, expr const & t); diff --git a/src/kernel/justification.h b/src/kernel/justification.h index a8434a9bf..3bd8b9764 100644 --- a/src/kernel/justification.h +++ b/src/kernel/justification.h @@ -61,7 +61,7 @@ public: justification(justification && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; } ~justification() { if (m_ptr) m_ptr->dec_ref(); } - operator bool() const { return m_ptr != nullptr; } + explicit operator bool() const { return m_ptr != nullptr; } justification_cell * raw() const { return m_ptr; } diff --git a/src/kernel/metavar.cpp b/src/kernel/metavar.cpp index 6c23de869..01d5c37f9 100644 --- a/src/kernel/metavar.cpp +++ b/src/kernel/metavar.cpp @@ -126,7 +126,7 @@ expr metavar_env::get_type(name const & m) { bool metavar_env::has_type(name const & m) const { auto it = const_cast(this)->m_metavar_data.splay_find(m); lean_assert(it); - return it->m_type; + return static_cast(it->m_type); } bool metavar_env::has_type(expr const & m) const { @@ -343,7 +343,7 @@ expr add_inst(expr const & m, unsigned s, expr const & v) { } bool has_local_context(expr const & m) { - return metavar_lctx(m); + return static_cast(metavar_lctx(m)); } expr pop_meta_context(expr const & m) { @@ -361,12 +361,12 @@ bool has_metavar(expr const & e, expr const & m, metavar_env const & menv) { if (has_metavar(e)) { lean_assert(is_metavar(m)); lean_assert(!menv.is_assigned(m)); - return find(e, [&](expr const & m2) { - return - is_metavar(m2) && - ((metavar_name(m) == metavar_name(m2)) || - (menv.is_assigned(m2) && has_metavar(menv.get_subst(m2), m, menv))); - }); + return static_cast(find(e, [&](expr const & m2) { + return + is_metavar(m2) && + ((metavar_name(m) == metavar_name(m2)) || + (menv.is_assigned(m2) && has_metavar(menv.get_subst(m2), m, menv))); + })); } else { return false; } diff --git a/src/kernel/object.h b/src/kernel/object.h index 51df40ea3..832c9c06c 100644 --- a/src/kernel/object.h +++ b/src/kernel/object.h @@ -98,7 +98,7 @@ public: object & operator=(object const & s) { LEAN_COPY_REF(object, s); } object & operator=(object && s) { LEAN_MOVE_REF(object, s); } - operator bool() const { return m_ptr != nullptr; } + explicit operator bool() const { return m_ptr != nullptr; } object_kind kind() const { return m_ptr->kind(); } diff --git a/src/kernel/occurs.cpp b/src/kernel/occurs.cpp index 4b6e65ede..1396c6f45 100644 --- a/src/kernel/occurs.cpp +++ b/src/kernel/occurs.cpp @@ -9,11 +9,11 @@ Author: Leonardo de Moura namespace lean { bool occurs(name const & n, context const * c, unsigned sz, expr const * es) { - return find(c, sz, es, [&](expr const & e) { return is_constant(e) && const_name(e) == n; }); + return static_cast(find(c, sz, es, [&](expr const & e) { return is_constant(e) && const_name(e) == n; })); } bool occurs(expr const & n, context const * c, unsigned sz, expr const * es) { - return find(c, sz, es, [&](expr const & e) { return e == n; }); + return static_cast(find(c, sz, es, [&](expr const & e) { return e == n; })); } bool occurs(expr const & n, expr const & m) { return occurs(n, nullptr, 1, &m); } bool occurs(name const & n, expr const & m) { return occurs(n, nullptr, 1, &m); } diff --git a/src/kernel/unification_constraint.h b/src/kernel/unification_constraint.h index d635f541d..de2c279e4 100644 --- a/src/kernel/unification_constraint.h +++ b/src/kernel/unification_constraint.h @@ -69,7 +69,7 @@ public: unification_constraint_kind kind() const { return m_ptr->kind(); } unification_constraint_cell * raw() const { return m_ptr; } - operator bool() const { return m_ptr != nullptr; } + explicit operator bool() const { return m_ptr != nullptr; } format pp(formatter const & fmt, options const & opts, pos_info_provider const * p = nullptr, bool include_justification = false) const { lean_assert(m_ptr); diff --git a/src/library/tactic/goal.h b/src/library/tactic/goal.h index fedded9bd..48b47c3c7 100644 --- a/src/library/tactic/goal.h +++ b/src/library/tactic/goal.h @@ -26,7 +26,7 @@ public: goal(hypotheses const & hs, expr const & c); hypotheses const & get_hypotheses() const { return m_hypotheses; } expr const & get_conclusion() const { return m_conclusion; } - operator bool() const { return m_conclusion; } + explicit operator bool() const { return static_cast(m_conclusion); } format pp(formatter const & fmt, options const & opts) const; name mk_unique_hypothesis_name(name const & suggestion) const; }; diff --git a/src/library/tactic/tactic.h b/src/library/tactic/tactic.h index acf1139d0..66606ab7d 100644 --- a/src/library/tactic/tactic.h +++ b/src/library/tactic/tactic.h @@ -74,7 +74,7 @@ public: tactic(tactic const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); } tactic(tactic && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; } ~tactic() { if (m_ptr) m_ptr->dec_ref(); } - operator bool() const { return m_ptr != nullptr; } + explicit operator bool() const { return m_ptr != nullptr; } friend void swap(tactic & a, tactic & b) { std::swap(a.m_ptr, b.m_ptr); } tactic & operator=(tactic const & s); tactic & operator=(tactic && s); diff --git a/src/util/list.h b/src/util/list.h index 33321b132..21bdb0a6e 100644 --- a/src/util/list.h +++ b/src/util/list.h @@ -79,7 +79,7 @@ public: cell * raw() const { return m_ptr; } /** \brief Return true iff it is not the empty/nil list. */ - operator bool() const { return m_ptr != nullptr; } + explicit operator bool() const { return m_ptr != nullptr; } friend bool is_nil(list const & l) { return l.m_ptr == nullptr; } friend bool empty(list const & l) { return is_nil(l); } diff --git a/src/util/name.h b/src/util/name.h index fc8ee0d76..2a8be053d 100644 --- a/src/util/name.h +++ b/src/util/name.h @@ -74,7 +74,7 @@ public: bool is_anonymous() const { return kind() == name_kind::ANONYMOUS; } bool is_string() const { return kind() == name_kind::STRING; } bool is_numeral() const { return kind() == name_kind::NUMERAL; } - operator bool() const { return !is_anonymous(); } + explicit operator bool() const { return !is_anonymous(); } unsigned get_numeral() const; /** \brief If the tail of the given hierarchical name is a string, then it returns this string. diff --git a/src/util/optional.h b/src/util/optional.h index 76db77b81..8761fc51d 100644 --- a/src/util/optional.h +++ b/src/util/optional.h @@ -40,7 +40,7 @@ public: m_value.~T(); } - operator bool() const { return m_some; } + explicit operator bool() const { return m_some; } T const * operator->() const { lean_assert(m_some); return &m_value; } T * operator->() { lean_assert(m_some); return &m_value; } T const & operator*() const { lean_assert(m_some); return m_value; } diff --git a/src/util/sexpr/format.h b/src/util/sexpr/format.h index 75fbf8a04..798637ef2 100644 --- a/src/util/sexpr/format.h +++ b/src/util/sexpr/format.h @@ -186,7 +186,7 @@ public: } unsigned hash() const { return m_value.hash(); } - operator bool() const { return m_value; } + explicit operator bool() const { return static_cast(m_value); } friend format compose(format const & f1, format const & f2); friend format nest(int i, format const & f); diff --git a/src/util/sexpr/sexpr.h b/src/util/sexpr/sexpr.h index cfaa6c6ad..b8d0023ea 100644 --- a/src/util/sexpr/sexpr.h +++ b/src/util/sexpr/sexpr.h @@ -60,7 +60,7 @@ public: sexpr_kind kind() const; - operator bool() const { return m_ptr != nullptr; } + explicit operator bool() const { return m_ptr != nullptr; } friend bool is_nil(sexpr const & s) { return s.m_ptr == nullptr; } friend sexpr const & head(sexpr const & s);