max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(library/local_context): typo

Browse source
This commit is contained in:
Leonardo de Moura 2016-03-05 16:57:15 -08:00
parent c0fc9e5479
commit fcf3e2e065
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/local_context.cpp
View file

@ -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_decl> local_context::get_local_decl(expr const & e) {
optional<local_decl> 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<local_decl>(*r);

2
src/library/local_context.h
View file

@ -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<local_decl> get_local_decl(expr const & e);
optional<local_decl> get_local_decl(expr const & e) const;
/** \brief Traverse local declarations based on the order they were created */
void for_each(std::function<void(local_decl const &)> const & fn) const;
optional<local_decl> find_if(std::function<bool(local_decl const &)> const & pred) const; // NOLINT