From ec5990f4de8b9a10937aeefc2b1ccf3aaca74c87 Mon Sep 17 00:00:00 2001 From: Rob Lewis Date: Mon, 14 Dec 2015 14:09:54 -0500 Subject: [PATCH] fix(library/norm_num): fix incorrect assert --- src/library/norm_num.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/library/norm_num.cpp b/src/library/norm_num.cpp index ccc888274..e778bddf1 100644 --- a/src/library/norm_num.cpp +++ b/src/library/norm_num.cpp @@ -603,7 +603,7 @@ expr norm_num_context::mk_norm_eq_pos_add_pos(expr & s_lhs, expr & s_rhs, expr & expr norm_num_context::mk_norm_eq_neg_mul_neg(expr & s_lhs, expr & s_rhs, expr & rhs) { lean_assert(is_neg_app(s_lhs)); lean_assert(is_neg_app(s_rhs)); - // lean_assert(is_neg_app(rhs)); // Leo: we get an assertion violation when testing norm_num1.lean + lean_assert(!is_neg_app(rhs)); auto s_lhs_v = get_type_and_arg_of_neg(s_lhs).second; expr s_rhs_v, type; std::tie(type, s_rhs_v) = get_type_and_arg_of_neg(s_rhs);