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

fix: #121 in the old frontend

Browse source 
This is temporary hack. We will delete this module in the near future.
This commit is contained in:
Leonardo de Moura 2020-03-06 12:12:23 -08:00
parent 8db309a079
commit 88a62f9f7e
2 changed files with 11 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/library/type_context.cpp
View file

@ -1918,8 +1918,16 @@ bool type_context_old::process_assignment(expr const & m, expr const & v) {
use_fo = true;
}
if (use_fo && (is_app(new_v) || !m_unifier_cfg.m_const_approx)) {
return process_assignment_fo_approx(mvar, args, new_v);
if (use_fo) {
if (is_app(new_v) || !m_unifier_cfg.m_const_approx) {
return process_assignment_fo_approx(mvar, args, new_v);
} else {
scope s(*this);
if (process_assignment_fo_approx(mvar, args, new_v)) {
s.commit();
return true;
}
}
}
if (optional<expr> new_new_v = check_assignment(locals, in_ctx_locals, mvar, new_v))

2
tests/lean/run/121.lean
View file

@ -2,7 +2,7 @@ abbrev DelabM := Id
abbrev Delab := DelabM Nat
example : DelabM Nat := pure 1 -- works
-- example : Delab := pure 1 -- fails in old frontend
example : Delab := pure 1 -- works
new_frontend