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

fix(library/congr_lemma): compilation error in debug mode

Browse source
This commit is contained in:
Leonardo de Moura 2016-07-10 10:37:27 -07:00
parent 2ae516ebe0
commit df113de725
1 changed files with 0 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/library/congr_lemma.cpp
View file

@ -335,7 +335,6 @@ struct congr_lemma_manager {
expr pr2 = mk_eq_refl(m_ctx, a);
for (; i < kinds.size(); i++) {
if (kinds[i] == congr_arg_kind::Cast && !pinfos[i].is_prop()) {
lean_assert(pinfos[i].is_subsingleton());
expr r1 = rhss1[i];
expr r2 = rhss[i];
expr r1_eq_r2 = mk_app(m_ctx, get_subsingleton_elim_name(), r1, r2);