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

fix: is_def_eq approximation

Browse source
This commit is contained in:
Leonardo de Moura 2019-12-13 10:29:30 -08:00
parent afc50a801d
commit 15c8b14aad
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/library/type_context.cpp
View file

@ -1918,8 +1918,9 @@ bool type_context_old::process_assignment(expr const & m, expr const & v) {
use_fo = true;
}
if (use_fo)
if (use_fo && is_app(new_v)) {
return process_assignment_fo_approx(mvar, args, new_v);
}
if (optional<expr> new_new_v = check_assignment(locals, in_ctx_locals, mvar, new_v))
new_v = *new_new_v;