From fcf3e2e065c38a48ea5830212cea7769d42dc086 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 5 Mar 2016 16:57:15 -0800 Subject: [PATCH] fix(library/local_context): typo --- src/library/local_context.cpp | 2 +- src/library/local_context.h | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/library/local_context.cpp b/src/library/local_context.cpp index 43a575c002..82bdb26ed7 100644 --- a/src/library/local_context.cpp +++ b/src/library/local_context.cpp @@ -79,7 +79,7 @@ expr local_context::mk_local_decl(name const & ppn, expr const & type, expr cons return mk_local_decl(mk_local_decl_name(), ppn, type, some_expr(value), binder_info()); } -optional local_context::get_local_decl(expr const & e) { +optional local_context::get_local_decl(expr const & e) const { lean_assert(is_local_decl_ref(e)); if (auto r = m_name2local_decl.find(mlocal_name(e))) return optional(*r); diff --git a/src/library/local_context.h b/src/library/local_context.h index 14b7543aca..883edab581 100644 --- a/src/library/local_context.h +++ b/src/library/local_context.h @@ -91,7 +91,7 @@ public: expr mk_local_decl(name const & ppn, expr const & type, expr const & value); /** \brief Return the local declarations for the given reference. \pre is_local_decl_ref(e) */ - optional get_local_decl(expr const & e); + optional get_local_decl(expr const & e) const; /** \brief Traverse local declarations based on the order they were created */ void for_each(std::function const & fn) const; optional find_if(std::function const & pred) const; // NOLINT