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

fix(library): compilation errors in debug mode

Browse source
This commit is contained in:
Leonardo de Moura 2016-03-18 14:26:21 -07:00
parent 9bc2fe04d2
commit 8d92d7bb46
2 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/local_context.h
View file

@ -35,7 +35,6 @@ private:
friend class local_context;
friend void initialize_local_context();
local_decl(unsigned idx, name const & n, name const & pp_n, expr const & t, optional<expr> const & v, binder_info const & bi);
unsigned get_idx() const { return m_ptr->m_idx; }
public:
local_decl();
local_decl(local_decl const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
@ -52,6 +51,7 @@ public:
optional<expr> const & get_value() const { return m_ptr->m_value; }
binder_info const & get_info() const { return m_ptr->m_bi; }
expr mk_ref() const;
unsigned get_idx() const { return m_ptr->m_idx; }
};
bool is_local_decl_ref(expr const & e);

3
src/library/type_context.cpp
View file

@ -190,7 +190,8 @@ expr type_context::revert_core(unsigned num, expr const * locals, expr const & m
expr type_context::revert(unsigned num, expr const * locals, expr const & mvar) {
lean_assert(is_metavar_decl_ref(mvar));
lean_assert(std::all_of(locals, locals+num, [&](expr const & l) { return mvar.get_context().contains(l); }));
lean_assert(std::all_of(locals, locals+num, [&](expr const & l) {
return static_cast<bool>(m_mctx.get_metavar_decl(mvar)->get_context().get_local_decl(l)); }));
buffer<expr> reverted;
expr new_mvar = revert_core(num, locals, mvar, reverted);
expr r = mk_app(new_mvar, reverted);