michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(frontends/lean/elaborator): unassigned metavariable when using nested begin-end blocks

Browse source 
Closes #454
This commit is contained in:
Leonardo de Moura 2015-02-28 09:03:56 -08:00
parent 10f1232296
commit c772d7bf84
2 changed files with 11 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/frontends/lean/elaborator.cpp
View file

@ -1578,15 +1578,13 @@ bool elaborator::try_using_begin_end(substitution & subst, expr const & mvar, pr
goals gs = ps.get_goals();
if (!gs)
throw_elaborator_exception("invalid nested begin-end block, there are no goals to be solved", ptac);
goal g = head(gs);
expr mvar = g.get_mvar();
proof_state focus_ps(ps, goals(g));
goal g = head(gs);
expr mvar = g.get_mvar();
name_generator ngen = ps.get_ngen();
proof_state focus_ps(ps, goals(g), ngen.mk_child());
if (!try_using_begin_end(subst, mvar, focus_ps, ptac))
return false;
substitution ps_new_subst = ps.get_subst();
name const & mvar_name = mlocal_name(mvar);
ps_new_subst.assign(mvar_name, *subst.get_expr(mvar_name));
ps = proof_state(ps, tail(gs), ps_new_subst);
ps = proof_state(ps, tail(gs), subst, ngen);
} else {
expr new_ptac = subst.instantiate_all(ptac);
if (auto tac = pre_tactic_to_tactic(new_ptac)) {

6
tests/lean/run/454.lean Normal file
View file

@ -0,0 +1,6 @@
constants (A : Type₁) (P : A → Type₁) (H : Π{a b : A}, P a → P b) (a b : A) (K : P a)
theorem foo : P b :=
begin
apply H, {apply K}
end