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

fix(frontends/lean): assertion violations

Browse source
This commit is contained in:
Leonardo de Moura 2014-09-16 18:59:51 -07:00
parent 78ad24a697
commit 2b0623c0a1
2 changed files with 3 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/frontends/lean/coercion_elaborator.cpp
View file

@ -17,7 +17,8 @@ coercion_elaborator::coercion_elaborator(coercion_info_manager & info, expr cons
list<constraints> const & choices, list<expr> const & coes,
bool use_id):
m_info(info), m_arg(arg), m_id(use_id), m_choices(choices), m_coercions(coes) {
lean_assert(length(m_coercions) + 1 == length(m_choices));
lean_assert(!use_id || length(m_coercions) + 1 == length(m_choices));
lean_assert(use_id || length(m_coercions) == length(m_choices));
}
optional<constraints> coercion_elaborator::next() {

2
src/frontends/lean/elaborator.cpp
View file

@ -419,8 +419,8 @@ public:
lean_assert(is_meta(f));
// let type checker add constraint
f_type = infer_type(f, cs);
lean_assert(is_pi(f_type));
f_type = m_tc[m_relax_main_opaque]->ensure_pi(f_type, f, cs);
lean_assert(is_pi(f_type));
}
} else {
erase_coercion_info(f);