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

feat(frontends/lean/parser): allow tactic to be used to fill holes in definitions

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-12-22 12:08:25 -08:00
parent 4229e498d2
commit 21d244d880
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/frontends/lean/parser.cpp
View file

@ -1872,7 +1872,7 @@ class parser::imp {
expr val = std::get<1>(r);
metavar_env menv = std::get<2>(r);
check_no_metavar(type, menv, "invalid definition, type still contains metavariables after elaboration");
if (!is_definition && has_metavar(val)) {
if (has_metavar(val)) {
val = apply_tactics(val, menv);
} else {
check_no_metavar(val, menv, "invalid definition, value still contains metavariables after elaboration");