michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(library/tmp_type_context): fixes #1033

Browse source 
This is just a workaround.
tmp_type_context is dead code in lean3.
This commit is contained in:
Leonardo de Moura 2016-03-28 09:38:22 -07:00
parent 6f74f65220
commit a07ad6df62
1 changed files with 2 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/library/tmp_type_context.cpp
View file

@ -57,7 +57,7 @@ optional<level> tmp_type_context::get_assignment(level const & u) const {
// 1- We should create the meta-variable using mk_uvar
// 2- We create using mk_idx_metauniv, and notify this object using
// set_next_uvar_idx
lean_assert(idx < m_uassignment.size());
if (idx >= m_uassignment.size()) return none_level();
return m_uassignment[idx];
}
@ -67,14 +67,13 @@ optional<expr> tmp_type_context::get_assignment(expr const & m) const {
// 1- We should create the meta-variable using mk_mvar
// 2- We create using mk_idx_metavar, and notify this object using
// set_next_mvar_idx
lean_assert(idx < m_eassignment.size());
if (idx >= m_eassignment.size()) return none_expr();
return m_eassignment[idx];
}
void tmp_type_context::update_assignment(level const & u, level const & v) {
unsigned idx = to_meta_idx(u);
lean_assert(idx < m_uassignment.size()); // see comments above
lean_assert(!m_uassignment[idx]);
m_uassignment[idx] = v;
if (!m_scopes.empty())
m_trail.emplace_back(trail_kind::Level, idx);