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

fix(library/rewriter): warning in release mode

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-01-17 15:46:49 -08:00
parent ba88a3b05a
commit 2434024272
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/rewriter/rewriter.cpp
View file

@ -53,8 +53,8 @@ pair<expr, expr> rewrite_lambda_type(environment const & env, context & ctx, exp
expr const & body = abst_body(v);
// expr const & pf_ty = result_ty.second;
expr const & new_v = mk_lambda(n, new_ty, body);
expr const & ty_ty = ti(ty, ctx);
lean_assert_eq(ty_ty, ti(new_ty, ctx)); // TODO(soonhok): generalize for hetreogeneous types
// expr const & ty_ty = ti(ty, ctx);
// lean_assert_eq(ty_ty, ti(new_ty, ctx)); // TODO(soonhok): generalize for hetreogeneous types
expr proof;
#if 0 // TODO(Leo): we don't have heterogeneous equality anymore
= mk_subst_th(ty_ty, ty, new_ty,