From 8e172afdc1d444b99aee315073c1be6e1bf582eb Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 9 Jan 2018 16:55:44 -0800 Subject: [PATCH] fix(library/type_context): typo --- src/library/type_context.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp index 28045cad4f..b26fdcf384 100644 --- a/src/library/type_context.cpp +++ b/src/library/type_context.cpp @@ -3145,7 +3145,7 @@ lbool type_context::is_def_eq_delta(expr const & t, expr const & s) { lean_trace(name({"type_context", "is_def_eq_detail"}), tout() << "unfold left&right: " << d_t->get_name() << "\n";); auto new_t = unfold_definition(t); auto new_s = unfold_definition(s); - if (*new_s && *new_t) + if (new_s && new_t) return to_lbool(is_def_eq_core_core(*new_t, *new_s)); else if (new_t) return to_lbool(is_def_eq_core_core(*new_t, s));