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

Attach elaborator the lean default parser

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-08-30 13:25:30 -07:00
parent 45d89ace65
commit 1e370023b1
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/frontends/lean/lean_parser.cpp
View file

@ -962,9 +962,9 @@ class parser::imp {
expr elaborate(expr const & e) {
if (has_metavar(e)) {
// TODO fix
regular(m_frontend) << e << endl;
throw parser_error("expression contains metavariables... not implemented yet.", m_last_cmd_pos);
expr r = m_elaborator(e);
m_elaborator.clear();
return r;
} else {
return e;
}