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

fix(library/type_context): typo

Browse source
This commit is contained in:
Leonardo de Moura 2018-01-09 16:55:44 -08:00
parent 5cd0f25c1e
commit 8e172afdc1
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/type_context.cpp
View file

@ -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));