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

chore(library/compiler/specialize): remove broken assertions

Browse source
This commit is contained in:
Leonardo de Moura 2019-08-16 09:46:05 -07:00
parent deecda22bd
commit dae30a4ea6
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/compiler/specialize.cpp
View file

@ -495,7 +495,7 @@ class specialize_fn {
/* Remark: we must not lambda abstract join points.
There is no risk of work duplication in this case, only code duplication. */
bool is_jp = is_join_point_name(decl.get_user_name());
lean_assert(!v || !is_irrelevant_type(m_st, m_lctx, decl.get_type()));
// lean_assert(!v || !is_irrelevant_type(m_st, m_lctx, decl.get_type()));
if (m_visited_not_in_binder.contains(x_name)) {
/* If `x` was already visited in a context outside of
a binder, then it is already in `m_ctx.m_vars`.